proposition: Lemma incl_app_inv : forall l1 l2 m : list A, incl (l1 ++ l2) m -> incl l1 m /\ incl l2 m.
proof: Proof. intro l1; induction l1 as [|a l1 IHl1]; intros l2 m Hin; split; auto. - apply incl_nil_l. - intros b Hb; inversion_clear Hb; subst; apply Hin. + now constructor. + simpl; apply in_cons. apply incl_appl with l1; [ apply incl_refl | assumption ]. - apply IHl1. now apply incl_cons_inv in Hin. Qed.
imports: PeanoNat