proposition: Lemma incl_cons_r : forall x : A, forall m l, l [= x :: m -> In x l \/ l [= m.
proof: Proof. induction l; simpl; intros. right. apply incl_nil. ded (incl_cons_l H). destruct H0. simpl in H0. destruct H0. auto. ded (IHl H1). destruct H2. auto. right. apply List.incl_cons; hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)