proposition: Lemma hom_merge_union_K: is_ihom h_merge_union_K h_merge_union_Ke xpred0.
proof: Proof. split; try (case; intros =>//=; by rewrite quot_union_KE quot_sameE). move=> v/=. rewrite quot_sameE/=. have x0 : F. { case: (repr v). exact: id. exact k. } etransitivity. apply: (reindex_onto (sum_left (fun _ : K => x0)) (@inl _ _)) => //. rewrite /= [X in X ≡ _]big_mkcond [X in _ ≡ X]big_mkcond /=. apply: eqv_bigr => [[x|x]] /= _. - rewrite eqxx andbT eqmodE. rewrite -{2}(reprK v) eqmodE. rewrite -equiv_clot_Kl. simpl. rewrite /map_equiv_rel/=. set (r := repr _). case r=>//= w. generalize (kh w). rewrite -eqmodE. move <-. by rewrite eqmodE. - rewrite andbC kv -[X in X ≡ _]/1. by case: ifP. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)