proposition: Lemma incl_app_elim : forall l1 l2 l3 : list A, l1 ++ l2 [= l3 -> l1 [= l3 /\ l2 [= l3.
proof: Proof. intuition. trans (l1 ++ l2). apply incl_appl. refl. hyp. trans (l1 ++ l2). apply incl_appr. refl. hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)