proposition: Lemma whites_add_sccs e x : let s := take (index x (stack e)) (stack e) in x \in grays e -> uniq (stack e) -> s \subset blacks e -> whites (add_sccs x e) = whites e.
proof: Proof. move=> /= x_gray se_uniq sb; rewrite /whites grays_add_sccs //=. by rewrite setUCA setUA setD1K. Qed.
imports: mathcomp(all_ssreflect) extra