proposition: Lemma topL (F: graph2): top·F ≃2 point (F ⊎ unit_graph 1%CM) (@unr _ _ F (unit_graph _) tt) (unl output).
proof: Proof. irewrite (merge_iso2 (union_C _ _))=>/=. etransitivity. refine (merge_iso2 (union_A _ _ _) _ _ _)=>/=. irewrite (merge_union_K_l (F:=F ⊎ _) _ _ (k:=fun x => unl input))=>//=. apply merge_nothing. by constructor. intros []. apply /eqquotP. eqv. Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)