proposition: Lemma merge_hom: is_ihom h_merge h.e h.d.
proof: Proof. split; intros=>/=. - rewrite endpoint_iso. symmetry. apply h_mergeE. - rewrite quot_sameE. symmetry. apply: (eqv_big_bij (f := h)); first exact: bij_perm_enum. + move=>x. rewrite eqmodE eqv_clot_map; last exact: bij_injective. apply/eqP/idP => [<-|/eqquotP ->]; by [exact: piK'|rewrite reprK]. + move=> x _. by rewrite vlabel_iso. - apply elabel_iso. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)