proposition: Lemma app_eq_cons : forall (A : Type) (z : A) (xs ys zs : list A), xs ++ ys = z :: zs -> (exists qs, xs = z :: qs /\ zs = qs ++ ys) \/ (xs = nil /\ ys = z :: zs).
proof: Proof. auto using cons_eq_app. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Metalib.CoqUniquenessTac