proposition: Lemma Rquo'_incl_RT : Rquo' << RT.
proof: Proof. unfold inclusion; intros. unfold RT. destruct topo_sortable_Rquo'. simpl. ded (l (nats_decr_lt dim)). destruct H0. intuition. apply H2. gen H; intro. unfold Rquo', Rquo, SCC'_tag in H; auto; do 3 destruct H; do 2 destruct H7. split; try split; try tauto; rewrite <- In_nats_decr_lt; eapply find_first_Some_bound; eauto. Qed.
imports: Coq(Permutation Multiset Heap PermutSetoid) CoLoR(AdjMat RelUtil ListExtras LogicUtil VecUtil NatUtil RelSub Path SortUtil ListNodup OptUtil BoundNat SCC SCC_dec Total)