proposition: Lemma in_elim : forall (x : A) l, In x l -> exists l1, exists l2, l = l1 ++ x :: l2.
proof: Proof. induction l; simpl; intros. contr. destruct H. subst x. exists nil. exists l. refl. ded (IHl H). do 2 destruct H0. rewrite H0. exists (a :: x0). exists x1. refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)