proposition: Lemma sub_visit e x : x \notin visited e -> subenv e (visit x e).
proof: Proof. move=> xNvisited; rewrite /subenv subxx/=; apply/andP; split; last first. by apply/forall_inP => y; rewrite !ffunE/=; case: ifP; rewrite ?ltnn. apply/forall_inP => y y_in; rewrite !ffunE/=. by case: (altP (y =P x)) xNvisited => // <-; rewrite inE y_in. Qed.
imports: mathcomp(all_ssreflect) extra_nocolors