proposition: Lemma SCC_effective_dec : forall M (H : M = SCC_mat_effective) x y, {SCC_effective H x y} + {~SCC_effective H x y}.
proof: Proof. intros. unfold SCC_effective. subst. unfold rel_on_dom. destruct (find_first (eq x) (eq_dec x)); auto with *. destruct (find_first (eq y) (eq_dec y)); auto with *. apply GoM_dec. Defined.
imports: CoLoR(GDomainBij AdjMat RelSub ListExtras RelUtil LogicUtil BoundNat SCC ListNodup)