proposition: Lemma sub_new_stack_new_visited e1 e2 : subenv e1 e2 -> wf_env e1 -> wf_env e2 -> (new_stack e1 e2) \subset (new_visited e1 e2).
proof: Proof. by move=> e1wf e2wf sube12; rewrite (@new_visitedE e1 e2)// subsetUl. Qed.
imports: mathcomp(all_ssreflect) extra_nocolors