@@ -15,6 +15,22 @@ data Elem : a -> List a -> Type where
1515 ||| Example: `the (Elem "b" ["a", "b"]) (There Here)`
1616 There : (later : Elem x xs) -> Elem x (y :: xs)
1717
18+||| `Here` will never equal `There`.
19+hereIsNotThere : Not (Here = There _)
20+hereIsNotThere Refl impossible
21+
22+||| If the tails don't match, neither will references to them.
23+tailMismatch : Not (this = that) -> Not (There this = There that)
24+tailMismatch f Refl = f Refl
25+
26+implementation DecEq (Elem x xs) where
27+ decEq Here Here = Yes Refl
28+ decEq Here (There later) = No hereIsNotThere
29+ decEq (There later) Here = No (hereIsNotThere . sym)
30+ decEq (There this) (There that) with (decEq this that)
31+ decEq (There this) (There this) | Yes Refl = Yes Refl
32+ decEq (There this) (There that) | No contra = No (tailMismatch contra)
33+
1834implementation Uninhabited (Elem {a} x []) where
1935 uninhabited Here impossible
2036 uninhabited (There p) impossible