proposition: Lemma cons_eq_app : forall (A : Type) (z : A) (xs ys zs : list A), z :: zs = xs ++ ys -> (exists qs, xs = z :: qs /\ zs = qs ++ ys) \/ (xs = nil /\ ys = z :: zs).
proof: Proof. destruct xs; intros ? ? H; simpl in *. auto. injection H. intros. subst. eauto. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Metalib.CoqUniquenessTac