proposition: Lemma merge_same'_hom: is_ihom (quot_same H: merge _ h -> merge _ k) bij_id xpred0.
proof: Proof. split; intros=>//; try (rewrite /=; apply/eqquotP; rewrite -H; apply: piK'). apply (eqv_big_bij (f := bij_id)) => //; first exact: bij_perm_enum. move => x. by rewrite -(reprK v) quot_sameE 2!eqmodE H. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)