proposition: Lemma iso_iso2' (F G: graph) (h: F ≃ G) (i o: F) (i' o': G): h i = i' -> h o = o' -> point F i o ≃2 point G i' o'.
proof: Proof. intros. Iso2 h. Defined.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)