@@ -570,11 +570,17 @@ Uninhabited a => Uninhabited (Vect (S n) a) where
570-- Properties
570-- Properties
571--------------------------------------------------------------------------------
571--------------------------------------------------------------------------------
573+vectMustBeNil : (xs : Vect Z a) -> xs = []
574+vectMustBeNil [] = Refl
573vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys)
576vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys)
574vectConsCong x xs xs Refl = Refl
577vectConsCong x xs xs Refl = Refl
576−vectMustBeNil : (xs : Vect Z a) -> xs = []
579+vectInjective1 : {xs : Vect n a} -> {ys : Vect m b} -> x :: xs ~=~ y :: ys -> x ~=~ y
577−vectMustBeNil [] = Refl
580+vectInjective1 Refl = Refl
582+vectInjective2 : {xs : Vect n a} -> {ys : Vect m b} -> x :: xs ~=~ y :: ys -> xs ~=~ ys
583+vectInjective2 Refl = Refl
579vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
585vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
580vectNilRightNeutral [] = Refl
586vectNilRightNeutral [] = Refl
@@ -671,12 +677,6 @@ transposeCons xs xss = rewrite zipWithIsLiftA2 Vect.(::) xs xss in rewrite trans
672--------------------------------------------------------------------------------
678--------------------------------------------------------------------------------
674−vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y
675−vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
677−vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys
678−vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl
680implementation DecEq a => DecEq (Vect n a) where
680implementation DecEq a => DecEq (Vect n a) where
681 decEq [] [] = Yes Refl
681 decEq [] [] = Yes Refl
682 decEq (x :: xs) (y :: ys) with (decEq x y)
682 decEq (x :: xs) (y :: ys) with (decEq x y)