@@ -570,11 +570,17 @@ Uninhabited a => Uninhabited (Vect (S n) a) where
570570-- Properties
571571--------------------------------------------------------------------------------
572572
573+vectMustBeNil : (xs : Vect Z a) -> xs = []
574+vectMustBeNil [] = Refl
575+
573576vectConsCong : (x : elem) -> (xs : Vect len elem) -> (ys : Vect m elem) -> (xs = ys) -> (x :: xs = x :: ys)
574577vectConsCong x xs xs Refl = Refl
575578
576−vectMustBeNil : (xs : Vect Z a) -> xs = []
577−vectMustBeNil [] = Refl
579+vectInjective1 : {xs : Vect n a} -> {ys : Vect m b} -> x :: xs ~=~ y :: ys -> x ~=~ y
580+vectInjective1 Refl = Refl
581+
582+vectInjective2 : {xs : Vect n a} -> {ys : Vect m b} -> x :: xs ~=~ y :: ys -> xs ~=~ ys
583+vectInjective2 Refl = Refl
578584
579585vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
580586vectNilRightNeutral [] = Refl
@@ -671,12 +677,6 @@ transposeCons xs xss = rewrite zipWithIsLiftA2 Vect.(::) xs xss in rewrite trans
671677-- DecEq
672678--------------------------------------------------------------------------------
673679
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
676−
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
679−
680680implementation DecEq a => DecEq (Vect n a) where
681681 decEq [] [] = Yes Refl
682682 decEq (x :: xs) (y :: ys) with (decEq x y)