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 e_wf; split=> /=; do ? by [exact: wf_sccs|rewrite whites_stackF ?wf_uniq]. move=> y; rewrite grays_add_stack // !inE. by case: (_ == _) colorP => [] []. Qed.
imports: mathcomp(all_ssreflect) bigmin extra