proposition: Lemma merge_subgraph_par (G : graph) (V1 V2 : {set G}) (E1 E2 : {set edge G}) (con1 : consistent V1 E1) (con2 : consistent V2 E2) (i1 o1 : subgraph_for con1) (i2 o2 : subgraph_for con2) : val i2 = val i1 -> val o2 = val o1 -> [disjoint E1 & E2] -> (forall x, x \in V1 -> x \in V2 -> x \in [set val i1; val o1]) -> point (subgraph_for con1) i1 o1 ∥ point (subgraph_for con2) i2 o2 ≃2 point (subgraph_for (consistentU con1 con2)) (Sub (val i1) (union_bij_proofL _ (valP i1))) (Sub (val o2) (union_bij_proofR _ (valP o2))).
proof: Proof. move => Ei Eo disE12 cap12. rewrite /par/=/g2_par. set G12 := (point _ _ _ ⊎ point _ _ _)%G. have eqvI (x : G) (inV1 : x \in V1) (inV2 : x \in V2) : inl (Sub x inV1) = inr (Sub x inV2) %[mod @eqv_clot G12 [:: (unl input, unr input); (unl output, unr output)]]. { case/set2P : (cap12 _ inV1 inV2) => ?; subst x; rewrite !valK' !/input !/output. rewrite -Ei in inV1 inV2 *. rewrite valK'. apply/eqquotP. by eqv. rewrite -Eo in inV1 inV2 *. rewrite valK'. apply/eqquotP. by eqv. } set x0 := Sub (sval i1) (union_bij_proofL V2 (valP i1)). rewrite /x0 /G12. apply: iso2_comp. apply: (iso_iso2 (merge_subgraph_iso eqvI disE12)). rewrite !(merge_subgraph_isoE eqvI disE12 x0). rewrite -> merge_nothing. 2: repeat constructor; exact: val_inj. apply: (iso_iso2' (h := iso_id)); apply: val_inj => /=; by rewrite val_insubd inE ?(valP i1) ?(valP o2). Qed.
imports: Coq(RelationClasses Morphisms Setoid) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(bij set_tac digraph sgraph minor checkpoint) GraphTheory(setoid_bigop structures pttdom mgraph mgraph2) GraphTheory(skeleton bounded equiv extraction_def)