proposition: Lemma merge_subgraph_dot (G : graph) (V1 V2 : {set G}) (E1 E2 : {set edge G}) (con1 : consistent V1 E1) (con2 : consistent V2 E2) i1 i2 o1 o2 : val o1 = val i2 -> [disjoint E1 & E2] -> (forall x, x \in V1 -> x \in V2 -> x = 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 => Eoi disE12 cap12. rewrite /dot/=/g2_dot. 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 output, unr input)]]. { move: (inV1) (inV2). rewrite (cap12 _ inV1 inV2) {2 4}Eoi /= => ? ?. rewrite !valK'. apply/eqquotP. exact: eqv_clot_hd. } 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)