proposition: Lemma SCC'_dec : forall x y, {SCC' x y} + {~SCC' x y}.
proof: Proof. intros. unfold SCC', clos_refl, union. destruct (eq_dec x y); auto. subst; destruct (In_dec eq_dec y Dom). left; auto. right; tauto. destruct (SCC_dec x y); destruct (In_dec eq_dec y Dom); destruct (In_dec eq_dec x Dom); rewrite <- SCC_effective_exact in *; try tauto. Defined.
imports: Coq(Permutation Multiset Heap PermutSetoid) CoLoR(AdjMat RelUtil ListExtras LogicUtil VecUtil NatUtil RelSub Path SortUtil ListNodup OptUtil BoundNat SCC SCC_dec Total)