proposition: Lemma app_com_incl : forall l1 l2 l3 l4 : list A, (l1 ++ l3) ++ l2 [= l4 -> (l1 ++ l2) ++ l3 [= l4.
proof: Proof. unfold incl. intros. apply H. apply in_app_com. hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)