@@ -378,7 +378,7 @@ scanl : (b -> a -> b) -> b -> List a -> List b
378378scanl f q [] = [q]
379379scanl f q (x::xs) = q :: scanl f (f q x) xs
380380
381−||| The scanl1 function is a variant of scanl that doesn't require an explicit
381+||| The scanl1 function is a variant of scanl that doesn't require an explicit
382382||| starting value.
383383||| It assumes the first element of the list to be the starting value and then
384384||| starts the fold with the element following it.
@@ -855,6 +855,10 @@ catMaybes (x::xs) =
855855-- Properties
856856--------------------------------------------------------------------------------
857857
858+||| (::) is injective
859+consInjective : (x :: xs) = (y :: ys) -> (x = y, xs = ys)
860+consInjective Refl = (Refl, Refl)
861+
858862||| The empty list is a right identity for append.
859863appendNilRightNeutral : (l : List a) ->
860864 l ++ [] = l