proposition: Lemma total_order_eq_midex: (forall l, exists R, transitive R /\ irreflexive R /\ total R l /\ rel_midex R) -> eq_midex A.
proof: Proof. do 3 intro. destruct (H (x::y::nil)). decompose [and] H0. destruct (H5 x y); destruct (H5 y x). absurd (x0 x x). apply H3. apply H1 with y; hyp. constructor 2. intro. rewrite H7 in H4. rewrite H7 in H6. contr. constructor 2. intro. rewrite H7 in H4. rewrite H7 in H6. contr. destruct (H2 x y); simpl; try tauto. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)