proposition: Lemma In_midex : eq_midex A -> forall (x : A) l, In x l \/ ~In x l.
proof: Proof. induction l. tauto. simpl. destruct (H a x); destruct IHl; tauto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)