proposition: Lemma add_blacks_ewf x e : x \in grays e -> wf_env e -> wf_env (add_blacks x e).
proof: Proof. move=> x_gray [s_def sccs_blacks s_uniq]; split => //=; last first. by rewrite subsetU // sccs_blacks orbT. apply/setP=> y; rewrite !inE. by have [->|] := altP (y =P x); case: colorP=> //=; case: colorP x_gray. Qed.
imports: mathcomp(all_ssreflect) extra