proposition: Lemma sub_visited e1 e2 : subenv e1 e2 -> visited e1 \subset visited e2.
proof: Proof. move=> sube12; apply/subsetP=> x; rewrite !inE => x_visited1. by rewrite (sub_snum sube12)// inE. Qed.
imports: mathcomp(all_ssreflect) extra_nocolors