proposition: Lemma hom_union_merge_l: is_ihom h_union_merge_l bij_id xpred0.
proof: Proof. split; try by case; intros=>//=; rewrite ?union_quot_lEl ?union_quot_lEr quot_sameE //. move=> x. rewrite /=quot_sameE. case:x=>[x|x]. have x0 := repr x. - pose f (z : F + G) := if z is inl z' then z' else x0. etransitivity. apply: (reindex_onto (@inl _ _) f) => /=. + move => [i|i] //=. by rewrite eq_sym eqmodE eqv_clot_map_lr. + rewrite [X in X ≡ _]big_mkcond [X in _ ≡ X]big_mkcond. apply: eqv_bigr => z _ => /=. rewrite eqmodE eqv_clot_map. 2: apply inl_inj. rewrite eqxx andbT -{2}(reprK x) eqmodE//. - apply (big_pred1 (inr x))=>y. rewrite eqmodE. case y=>z. + by rewrite eqv_clot_map_lr. + apply eqv_clot_map_eq. by rewrite inr_codom_inl. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)