proposition: Lemma in_app_com : forall (x : A) l1 l2 l3, In x ((l1 ++ l3) ++ l2) -> In x ((l1 ++ l2) ++ l3).
proof: Proof. intros. rewrite !in_app in H. intuition. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)