proposition: Lemma inj_sewr : injective sewr.
proof: Proof. move=> xr yr /eqP; rewrite /sewr. case: (in_bGr xr) (in_bGr yr) => [[xd0 b_xr] | b'xr] [[xd1 b_yr] | b'yr] //=. by move/eqP/inj_sewd/(congr1 (hdr xr)); rewrite !hdr_hrd. by rewrite eq_Tagged -val_eqE /= => /eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color patch)