@@ -861,6 +861,12 @@ catMaybes (x::xs) =
861861-- Properties
862862--------------------------------------------------------------------------------
863863
864+Uninhabited ([] = _ :: _) where
865+ uninhabited Refl impossible
866+
867+Uninhabited (_ :: _ = []) where
868+ uninhabited Refl impossible
869+
864870||| (::) is injective
865871consInjective : {x : a} -> {xs : List a} -> {y : b} -> {ys : List b} ->
866872 (x :: xs) = (y :: ys) -> (x = y, xs = ys)