proposition: Lemma iso2_subgraph_forT (G : graph2) (V : {set G}) (E : {set edge G}) (con : consistent V E) i o : (forall x, x \in V) -> (forall e, e \in E) -> val i = input -> val o = output -> point (subgraph_for con) i o ≃2 G.
proof: Proof. move => HV HE Hi Ho. have ? : V = [set: G] by apply/setP => z; rewrite inE HV. have ? : E = [set: edge G] by apply/setP => z; rewrite inE HE. subst. transitivity (point (subgraph_for (@consistentTT _ _ G)) i o). - exact: subgraph_for_iso. - irewrite (iso_iso2 (iso_subgraph_forT _)). rewrite /= Ho Hi. by case G. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)