proposition: Lemma in_appr : forall (x : A) l1 l2, In x l2 -> In x (l1 ++ l2).
proof: Proof. induction l1; simpl; intros. hyp. right. apply IHl1. hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)