proposition: Lemma In_elim_right : eq_midex A -> forall (x : A) l, In x l -> exists l', exists l'', l = l'++x::l'' /\ ~In x l''.
proof: Proof. induction l; simpl; intros. contr. destruct (In_midex H x l). destruct IHl. hyp. destruct H2. ex (a::x0) x1. rewrite (proj1 H2), <- (app_comm_cons x0 (x::x1) a). tauto. destruct H0. ex (@nil A) l. simpl. rewrite H0. tauto. contr. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)