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