proposition: Lemma subgraph_for_iso (G : graph2) V1 V2 E1 E2 i1 i2 o1 o2 (C1 : @consistent _ _ G V1 E1) (C2: consistent V2 E2) : V1 = V2 -> E1 = E2 -> val i1 = val i2 -> val o1 = val o2 -> point (subgraph_for C1) i1 o1 ≃2 point (subgraph_for C2) i2 o2.
proof: Proof. move => eq_V eq_E eq_i eq_o. subst. move/val_inj : eq_i => ->. move/val_inj : eq_o => ->. unshelve Iso2 (@Iso _ _ (subgraph_for C1) (subgraph_for C2) bij_id bij_id xpred0 _). split=>//e b//=. by apply val_inj. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)