[ more ] missing results

libs/base/Data/Vect.idr

@@ -49,6 +49,11 @@ Biinjective Vect.(::) where
 -- Indexing into vectors
 --------------------------------------------------------------------------------
 
+export
+invertVectZ : (xs : Vect Z a) -> xs === []
+invertVectZ [] = Refl
+
+
 ||| All but the first element of the vector
 |||
 ||| ```idris example
@@ -67,6 +72,10 @@ public export
 head : Vect (S len) elem -> elem
 head (x::_) = x
 
+export
+invertVectS : (xs : Vect (S n) a) -> xs === head xs :: tail xs
+invertVectS (_ :: _) = Refl
+
 ||| The last element of the vector
 |||
 ||| ```idris example

libs/base/Data/Vect/Quantifiers.idr

@@ -155,6 +155,17 @@ namespace All
   forgetRememberId [] = Refl
   forgetRememberId (x :: xs) = cong (x ::) (forgetRememberId xs)
 
+  public export
+  castAllConst : {0 xs, ys : Vect n a} -> All (const ty) xs -> All (const ty) ys
+  castAllConst [] = rewrite invertVectZ ys in []
+  castAllConst (x :: xs) = rewrite invertVectS ys in x :: castAllConst xs
+
+  export
+  rememberForgetId : (vs : All (const ty) xs) ->
+    castAllConst (remember (forget vs)) === vs
+  rememberForgetId [] = Refl
+  rememberForgetId (x :: xs) = cong (x ::) (rememberForgetId xs)
+
   export
   zipPropertyWith : (f : {0 x : a} -> p x -> q x -> r x) ->
                     All p xs -> All q xs -> All r xs
@@ -232,4 +243,3 @@ namespace All
   drop' 0 ys = rewrite minusZeroRight k in ys
   drop' (S k) [] = []
   drop' (S k) (y :: ys) = drop' k ys
-