@@ -154,3 +154,29 @@ instance DecEq a => DecEq (List a) where
154154 decEq (x :: xs) (y :: ys) | (No p) | (No p') = No (\eq => lemma_x_neq_xs_neq p p' eq)
155155
156156
157+--------------------------------------------------------------------------------
158+-- Vect
159+--------------------------------------------------------------------------------
160+
161+total
162+vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y
163+vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} refl = refl
164+
165+total
166+vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys
167+vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} refl = refl
168+
169+total
170+vectLemma : {xs, ys : Vect n a} -> {x, y : a} -> x = y -> xs = ys -> x :: xs = y :: ys
171+vectLemma {xs=xs} {ys=xs} {x=x} {y=x} refl refl = refl
172+
173+total
174+vectDecEq : DecEq a => (x1 : Vect n a) -> (x2 : Vect n a) -> Dec (x1 = x2)
175+vectDecEq [] [] = Yes refl
176+vectDecEq (x :: xs) (y :: ys) with (decEq x y, vectDecEq xs ys)
177+ vectDecEq (x :: xs) (x :: xs) | (Yes eqHd, Yes eqTl) = Yes (vectLemma eqHd eqTl)
178+ vectDecEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))
179+ vectDecEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))
180+
181+instance DecEq a => DecEq (Vect n a) where
182+ decEq = vectDecEq