proposition: Lemma topR (F: graph2): F·top ≃2 point (F ⊎ unit_graph 1%CM) (unl input) (@unr _ _ F (unit_graph _) tt).
proof: Proof. irewrite (merge_iso2 (union_iso iso_id (union_C _ _))). irewrite (merge_iso2 (union_A _ _ _)). irewrite (merge_union_K_l (F:=F ⊎ _) _ _ (k:=fun x => unl output))=>//=. apply merge_nothing. by constructor. case. 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)