proposition: Lemma add_stack_pre e w : access_to e [set w] -> wf_env e -> w \in whites e -> wf_graph e -> access_to (add_stack w e) [set x in successors w].
proof: Proof. move=> grays_to e_wf w_white e_gwf. move=> x; rewrite grays_add_stack // 2?inE => /predU1P [->|]. by move=> y; rewrite inE => y_succ_w; rewrite connect1. move=> /grays_to x_to_y y; rewrite inE => y_succ_w. by rewrite (connect_trans _ (connect1 y_succ_w)) // x_to_y ?inE. Qed.
imports: mathcomp(all_ssreflect) extra