proposition: Lemma SCC'_tag_exact : forall x y, SCC' x y <-> SCC'_tag x = SCC'_tag y /\ SCC'_tag x <> None.
proof: Proof. intros. split; intros. unfold SCC'_tag in *. split. apply find_first_indep. intros. split; intros; eapply SCC'_trans; auto; eauto. apply SCC'_sym; auto. eapply find_first_exist; unfold SCC' in *. 2: ehyp. tauto. destruct H. assert (exists n, SCC'_tag x = Some n). destruct (SCC'_tag x); try tauto. exists n; tauto. destruct H1. gen H1; intro. rewrite H in H2. unfold SCC'_tag in H1. unfold SCC'_tag in H2. ded (In_find_first2 H1). ded (In_find_first2 H2). do 2 (destruct H3; destruct H4). rewrite H3 in H4. inversion H4. subst x1. eapply SCC'_trans. ehyp. apply SCC'_sym. auto. Qed.
imports: Coq(Permutation Multiset Heap PermutSetoid) CoLoR(AdjMat RelUtil ListExtras LogicUtil VecUtil NatUtil RelSub Path SortUtil ListNodup OptUtil BoundNat SCC SCC_dec Total)