Library ListFacts
Assorted facts about lists that are not in Coq's standard library.
Implicit arguments are declared by default in this library.
Implicit arguments are declared by default in this library.
Lemma cons_eq_app : ∀ (A : Type) (z : A) (xs ys zs : list A),
z :: zs = xs ++ ys →
(∃ qs, xs = z :: qs ∧ zs = qs ++ ys) ∨
(xs = nil ∧ ys = z :: zs).
Lemma app_eq_cons : ∀ (A : Type) (z : A) (xs ys zs : list A),
xs ++ ys = z :: zs →
(∃ qs, xs = z :: qs ∧ zs = qs ++ ys) ∨
(xs = nil ∧ ys = z :: zs).
Lemma nil_eq_app : ∀ (A : Type) (xs ys : list A),
nil = xs ++ ys →
xs = nil ∧ ys = nil.
Lemma app_cons_not_nil : ∀ (A : Type) (y : A) (xs ys : list A),
xs ++ y :: ys ≠ nil.
Lemma InA_In : ∀ (A : Type) (x : A) (xs : list A),
InA (@eq _) x xs → In x xs.
Lemma InA_iff_In : ∀ (A : Type) (x : A) (xs : list A),
InA (@eq _) x xs ↔ In x xs.
This page has been generated by coqdoc