proposition: Lemma iso2_GTG (G H : graph2) : G · top · H ≃2 point (G ⊎ H) (unl input) (unr output).
proof: Proof. rewrite-> topR. setoid_rewrite-> (merge_iso2 (iso_sym (union_A _ _ _))) => /=. setoid_rewrite-> (merge_iso2 (union_iso iso_id (union_C _ _))) => /=. rewrite-> (merge_iso2 (union_A _ _ _)) => /=. rewrite-> (merge_union_K_l (fun _ => unr input))=>//. 2: case; apply/eqquotP; by eqv. apply: merge_nothing. by repeat constructor. Qed.
imports: Coq(RelationClasses Morphisms Setoid) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries set_tac) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(equiv setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 ptt mgraph2_tw2 skeleton) GraphTheory(bounded extraction_def extraction_iso excluded)