@@ -99,4 +99,58 @@ instance DecEq (Fin n) where
9999 | Yes p = Yes $ cong p
100100 | No p = No $ \h => p $ fSinjective {f = f} {f' = f'} h
101101
102+--------------------------------------------------------------------------------
103+-- Tuple
104+--------------------------------------------------------------------------------
105+
106+lemma_both_neq : {x : a, y : b, x' : c, y' : d} -> (x = x' -> _|_) -> (y = y' -> _|_) -> ((x, y) = (x', y') -> _|_)
107+lemma_both_neq p_x_not_x' p_y_not_y' refl = p_x_not_x' refl
108+
109+lemma_snd_neq : {x : a, y : b, y' : d} -> (x = x) -> (y = y' -> _|_) -> ((x, y) = (x, y') -> _|_)
110+lemma_snd_neq refl p refl = p refl
111+
112+lemma_fst_neq_snd_eq : {x : a, x' : b, y : c, y' : d} ->
113+ (x = x' -> _|_) ->
114+ (y = y') ->
115+ ((x, y) = (x', y) -> _|_)
116+lemma_fst_neq_snd_eq p_x_not_x' refl refl = p_x_not_x' refl
117+
118+instance (DecEq a, DecEq b) => DecEq (a, b) where
119+ decEq (a, b) (a', b') with (decEq a a')
120+ decEq (a, b) (a, b') | (Yes refl) with (decEq b b')
121+ decEq (a, b) (a, b) | (Yes refl) | (Yes refl) = Yes refl
122+ decEq (a, b) (a, b') | (Yes refl) | (No p) = No (\eq => lemma_snd_neq refl p eq)
123+ decEq (a, b) (a', b') | (No p) with (decEq b b')
124+ decEq (a, b) (a', b) | (No p) | (Yes refl) = No (\eq => lemma_fst_neq_snd_eq p refl eq)
125+ decEq (a, b) (a', b') | (No p) | (No p') = No (\eq => lemma_both_neq p p' eq)
126+
127+
128+--------------------------------------------------------------------------------
129+-- List
130+--------------------------------------------------------------------------------
131+
132+lemma_val_not_nil : {x : t, xs : List t} -> ((x :: xs) = Prelude.List.Nil {a = t} -> _|_)
133+lemma_val_not_nil refl impossible
134+
135+lemma_x_eq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y) -> (xs = ys -> _|_) -> ((x :: xs) = (y :: ys) -> _|_)
136+lemma_x_eq_xs_neq refl p refl = p refl
137+
138+lemma_x_neq_xs_eq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> _|_) -> (xs = ys) -> ((x :: xs) = (y :: ys) -> _|_)
139+lemma_x_neq_xs_eq p refl refl = p refl
140+
141+lemma_x_neq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> _|_) -> (xs = ys -> _|_) -> ((x :: xs) = (y :: ys) -> _|_)
142+lemma_x_neq_xs_neq p p' refl = p refl
143+
144+instance DecEq a => DecEq (List a) where
145+ decEq [] [] = Yes refl
146+ decEq (x :: xs) [] = No lemma_val_not_nil
147+ decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil)
148+ decEq (x :: xs) (y :: ys) with (decEq x y)
149+ decEq (x :: xs) (x :: ys) | Yes refl with (decEq xs ys)
150+ decEq (x :: xs) (x :: xs) | (Yes refl) | (Yes refl) = Yes refl -- maybe another yes refl
151+ decEq (x :: xs) (x :: ys) | (Yes refl) | (No p) = No (\eq => lemma_x_eq_xs_neq refl p eq)
152+ decEq (x :: xs) (y :: ys) | No p with (decEq xs ys)
153+ decEq (x :: xs) (y :: xs) | (No p) | (Yes refl) = No (\eq => lemma_x_neq_xs_eq p refl eq)
154+ decEq (x :: xs) (y :: ys) | (No p) | (No p') = No (\eq => lemma_x_neq_xs_neq p p' eq)
155+
102156