@@ -861,6 +861,12 @@ catMaybes (x::xs) =
861-- Properties
861-- Properties
862--------------------------------------------------------------------------------
862--------------------------------------------------------------------------------
864+Uninhabited ([] = _ :: _) where
865+ uninhabited Refl impossible
867+Uninhabited (_ :: _ = []) where
868+ uninhabited Refl impossible
864||| (::) is injective
870||| (::) is injective
865consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
871consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
866 (x :: xs) = (y :: ys) -> (x = y, xs = ys)
872 (x :: xs) = (y :: ys) -> (x = y, xs = ys)