proposition: Lemma elim_incl_app : forall (A : Type) (xs ys zs : list A), incl (xs ++ ys) zs -> incl xs zs /\ incl ys zs.
proof: Proof. unfold incl. auto with datatypes. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Metalib.CoqUniquenessTac