proposition: Lemma Rquo'_path : forall l x y, path Rquo' x y l -> exists r, SCC'_tag r = Some x /\ exists s, SCC'_tag s = Some y /\ R! r s.
proof: Proof. induction l; intros; simpl in *. unfold Rquo', Rquo in H. do 2 destruct H. exists x0; intuition. destruct H2; exists x1; intuition. destruct H. unfold Rquo', Rquo in H. do 2 destruct H. exists x0; intuition. destruct H3; destruct H. ded (IHl _ _ H0). do 2 destruct H4. do 2 destruct H5; exists x3. intuition. eapply t_trans; eauto. destruct (eq_dec x1 x2). subst x1. apply t_step. auto. eapply t_trans. apply t_step. eauto. cut (SCC' x1 x2). intros. do 2 destruct H7; try tauto. destruct H7; auto. rewrite SCC'_tag_exact. intuition. congruence. rewrite H in H7. discr. Qed.
imports: Coq(Permutation Multiset Heap PermutSetoid) CoLoR(AdjMat RelUtil ListExtras LogicUtil VecUtil NatUtil RelSub Path SortUtil ListNodup OptUtil BoundNat SCC SCC_dec Total)