proposition: Lemma topo_sortable_Rquo' : topo_sortable Rquo'.
proof: Proof. apply antisym_topo_sortable_topo_sortable. apply possible_antisym_topo_sort; auto. unfold RelMidex.eq_dec; apply eq_nat_dec. unfold rel_dec; apply Rquo'_dec. apply irrefl_tc_Rquo'. Qed.
imports: Coq(Permutation Multiset Heap PermutSetoid) CoLoR(AdjMat RelUtil ListExtras LogicUtil VecUtil NatUtil RelSub Path SortUtil ListNodup OptUtil BoundNat SCC SCC_dec Total)