proposition: Lemma par_component (G : graph) (H : graph2) : point (G ⊎ g2_top) (inr input) (inr output) ∥ H ≃2 point (G ⊎ H) (inr input) (inr output).
proof: Proof. rewrite-> par2C. setoid_rewrite-> (merge_iso2 (union_A _ _ _)) =>/=. rewrite-> (merge_union_K_l (fun x: two_graph _ _ => if x then unl input else unl output))=>//=. setoid_rewrite-> (merge_iso2 (union_C _ _)) =>/=. apply merge_nothing. by repeat constructor. by case. move => [[]|[]] /=; apply/eqquotP; eqv. 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)