fact: Definition outenv (roots : {set V}) (e e' : env) := [/\ {in new_stack e e' &, gconnected}, {in new_stack e e', forall x, exists2 y, y \in stack e & gconnect x y} & visited e' = visited e :|: nexts (~: visited e) roots ].
imports: mathcomp(all_ssreflect) extra_nocolors