proposition: Lemma merge2_surj (G: graph2) (r: equiv_rel G) (H: graph2) (fv : G -> H) (fv': H -> G) (fe : bij (edge G) (edge H)) fd : (forall x y, reflect (kernel fv x y) (r x y)) -> cancel fv' fv -> is_hom fv fe fd -> fv input = input -> fv output = output -> merge2 G r ≃2 H.
proof: Proof. intros H1 H2 H3 I O. Iso2 (merge_surj H1 H2 H3); by rewrite merge_surjE. Defined.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij equiv) GraphTheory(setoid_bigop structures pttdom mgraph ptt)