proposition: Lemma hom_merge_merge: is_ihom (quot_quot e': merge _ e' -> merge F _) bij_id xpred0.
proof: Proof. split; intros=>//=; first by rewrite -equiv_comp_pi. rewrite [X in X ≡ _](partition_big (fun x => \pi x) (fun w => \pi w == v)). - apply: eqv_bigr => w pw. apply: eqv_big => x //. case: (altP (\pi x =P w)) => // ?. subst w. by rewrite -(eqP pw) quot_quotE eqxx. - move => x. by rewrite -[v]reprK -[repr v]reprK quot_quotE !eqmodE. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)