@@ -12,11 +12,6 @@ using (xs : List a)
1212 uninhabited Here impossible
1313 uninhabited (There p) impossible
1414
15− private
16− mkNo : ((x = y) -> _|_) -> (Elem x xs -> _|_) -> Elem x (y :: xs) -> _|_
17− mkNo f g Here = f refl
18− mkNo f g (There x) = g x
19−
2015 isElem : DecEq a => (x : a) -> (xs : List a) -> Dec (Elem x xs)
2116 isElem x [] = No absurd
2217 isElem x (y :: xs) with (decEq x y)
@@ -24,5 +19,12 @@ using (xs : List a)
2419 isElem x (y :: xs) | (No contra) with (isElem x xs)
2520 isElem x (y :: xs) | (No contra) | (Yes prf) = Yes (There prf)
2621 isElem x (y :: xs) | (No contra) | (No f) = No (mkNo contra f)
22+ where
23+ mkNo : {xs' : List a} ->
24+ ((x' = y') -> _|_) -> (Elem x' xs' -> _|_) ->
25+ Elem x' (y' :: xs') -> _|_
26+ mkNo f g Here = f refl
27+ mkNo f g (There x) = g x
28+
2729
2830