proposition: Lemma iso2_TGT (G : graph2) : top · G · top ≃2 point (G ⊎ g2_top) (inr input) (inr output).
proof: Proof. rewrite-> topL, topR => /=. Iso2 (iso_sym (union_A _ _ _)). 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)