proposition: Lemma total_order_eq_dec : {F : list A -> A -> A -> bool | forall l, let G := fun x y => F l x y = true in transitive G /\ irreflexive G /\ total G l} -> eq_dec A.
proof: Proof. unfold transitive, irreflexive, total, trichotomy. intros H x y. destruct H. pose (a (x::y::nil)). assert ({x0 (x::y::nil) x y=true}+{x0 (x::y::nil) x y=false}). case (x0 (x::y::nil) x y); tauto. assert ({x0 (x::y::nil) y x=true}+{x0 (x::y::nil) y x=false}). case (x0 (x::y::nil) y x); tauto. destruct a0. destruct H2. pose (H3 x y). simpl in o. destruct H. constructor 2. intro. rewrite H in e. rewrite H in H2. exact (H2 y e). destruct H0. constructor 2. intro. rewrite H in e0. rewrite H in H2. exact (H2 y e0). constructor. destruct o; try tauto. rewrite H in e. inversion e. destruct H. hyp. rewrite H in e0. inversion e0. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)