proposition: Lemma incl_appl_incl : forall l1 l2 l3 : list A, l1 ++ l2 [= l3 -> l2 [= l3.
proof: Proof. induction l1; intros. hyp. trans ((a::l1) ++ l2). 2: hyp. apply incl_appr. refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)