Idris2Doc : Data.List.Equalities

# Data.List.Equalities

SnocNonEmpty : (xs : Lista) -> (x : a) -> NonEmpty (snocxsx)
`  Proof that snoc'ed list is not empty in terms of `NonEmpty`.`

Totality: total
appendCong2 : x1 = y1 -> x2 = y2 -> x1++x2 = y1++y2
`  Appending pairwise equal lists gives equal lists`

Totality: total
appendNonEmptyLeftNotEq : (zs : Lista) -> (xs : Lista) -> NonEmptyxs => Not (zs = xs++zs)
`  List cannot be equal to itself prepended with some non-empty list.`

Totality: total
appendNonEmptyRightNotEq : (zs : Lista) -> (xs : Lista) -> NonEmptyxs => Not (zs = zs++xs)
`  List cannot be equal to itself appended with some non-empty list.`

Totality: total
appendSameLeftInjective : (xs : Lista) -> (ys : Lista) -> (zs : Lista) -> zs++xs = zs++ys -> xs = ys
`  Appending the same list at left is injective.`

Totality: total
appendSameRightInjective : (xs : Lista) -> (ys : Lista) -> (zs : Lista) -> xs++zs = ys++zs -> xs = ys
`  Appending the same list at right is injective.`

Totality: total
consCong2 : x = y -> xs = ys -> x::xs = y::ys
`  Two lists are equal, if their heads are equal and their tails are equal.`

Totality: total
lengthDistributesOverAppend : (xs : Lista) -> (ys : Lista) -> length (xs++ys) = lengthxs+lengthys
`  List.length is distributive over appending.`

Totality: total
lengthSnoc : (x : a) -> (xs : Lista) -> length (snocxsx) = S (lengthxs)
`  Length of a snoc'd list is the same as Succ of length list.`

Totality: total
mapDistributesOverAppend : (f : (a -> b)) -> (xs : Lista) -> (ys : Lista) -> mapf (xs++ys) = mapfxs++mapfys
`  List.map is distributive over appending.`

Totality: total
snocInjective : snocxsx = snocysy -> (xs = ys, x = y)
`  Equal non-empty lists should result in equal components after destructuring 'snoc'.`

Totality: total
snocNonEmpty : Not (xs++ [x] = [])
`  A list constructued using snoc cannot be empty.`

Totality: total