proposition: Lemma Walkup_seq (p : seq G) : z \notin p -> {q : seq G' | map val q = p}.
proof: Proof. move=> p'z; exists (pmap insub p); rewrite (pmap_filter (insubK _)). by apply/all_filterP/allP=> x p_x; rewrite insubT //= (memPn p'z). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap)