proposition: Lemma white_add_sccs e x : let s := take (index x (stack e)) (stack e) in x \in gray e -> uniq (stack e) -> s \subset black e -> white (add_sccs x e) = white e.
proof: Proof. move=> /= x_gray se_uniq sb; rewrite whiteE gray_add_sccs //=. by rewrite setUCA setUA setD1K. Qed.
imports: mathcomp(all_ssreflect) bigmin extra