proposition: Lemma add_stack_ewf x e : x \in whites e -> wf_env e -> wf_env (add_stack x e).
proof: Proof. move=> x_white [s_def sccs_blacks s_uniq]; split => //=; last by rewrite whites_stackF. apply/setP=> y; rewrite !inE. by have [->|] := altP (y =P x); case: colorP=> //=; case: colorP x_white. Qed.
imports: mathcomp(all_ssreflect) extra