proposition: Lemma irrefl_tc_Rquo' : irreflexive (Rquo'!).
proof: Proof. unfold irreflexive. intuition. ded (clos_trans_path H). destruct H0 as [l]. destruct l. simpl in H0; destruct H0; auto. simpl in H0; destruct H0. ded (Rquo'_path l n x H1). do 2 destruct H2. do 2 destruct H3. unfold Rquo' in H0. destruct H0. unfold Rquo in H0. do 2 destruct H0. do 2 destruct H6. cut (R! x3 x2). intro. cut (x=n). intuition. cut (SCC' x3 x2). intro. rewrite SCC'_tag_exact in H9. destruct H9; congruence. unfold SCC'. intuition; ded (restriction x2 x3); try tauto. right. split; auto. apply t_step; auto. cut(R# x3 x2). intro. ded (rtc_split H8). destruct H9; try tauto. subst x3; congruence. assert (R# x3 x0). cut (SCC' x3 x0). intro. do 2 destruct H8. subst x3; intuition. destruct H8. apply tc_incl_rtc. intuition. rewrite SCC'_tag_exact. split. congruence. rewrite H6. discr. eapply rt_trans; eauto. assert (R# x0 x1). apply tc_incl_rtc. intuition. eapply rt_trans; eauto. cut (SCC' x1 x2). intro. do 2 destruct H10. subst x1; intuition. destruct H10. apply tc_incl_rtc. intuition. rewrite SCC'_tag_exact. split. congruence. rewrite H3. 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)