proposition: Lemma rel_dec_topo_sortable_eq_dec : forall R, rel_dec R -> topo_sortable R -> eq_dec A.
proof: Proof. intros R Rd H. apply total_order_eq_dec. exists (let (first,second):=H in first). destruct H. intro. pose (l l0). destruct l1. split; tauto. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)