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