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