This module contains stuff that may use functions from `Data.List`. This separation is needed because `Data.List` uses `List1` type inside it, thus the core of `List1` must not import `Data.List`.
import public Data.Maybe
consInjective : x ::: xs = y ::: ys -> (x = y, xs = ys)
listLength : (xs : List1 a) -> length xs = length (forget xs)
Proof that the length of a List1 is the same as the length
of the List it represents.
appendlNilRightNeutral : (l : List1 a) -> appendl l  = l
lappendNilLeftNeutral : (l : List1 a) -> lappend  l = l
appendAssociative : (l : List1 a) -> (c : List1 a) -> (r : List1 a) -> l ++ (c ++ r) = (l ++ c) ++ r
toListAppendl : (xs : List1 a) -> (ys : List a) -> toList (appendl xs ys) = forget xs ++ ys
toListLappend : (xs : List a) -> (ys : List1 a) -> toList (lappend xs ys) = xs ++ forget ys
toListAppend : (xs : List1 a) -> (ys : List1 a) -> toList (xs ++ ys) = toList xs ++ toList ys
fromListAppend : (xs : List a) -> (ys : List a) -> fromList (xs ++ ys) = fromList xs <+> fromList ys