proposition: Lemma in_elim_dec : forall (x : A) l, In x l -> exists m, exists p, l = m ++ x :: p /\ ~In x m.
proof: Proof. induction l; simpl; intros. contr. destruct H. subst x. exists nil. exists l. intuition. ded (IHl H). do 3 destruct H0. subst l. case (eqA_dec a x); intro. subst x. exists nil. exists (x0 ++ a :: x1). intuition. exists (a :: x0). exists x1. intuition. simpl in H2. destruct H2; auto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)