proposition: Lemma eqv_clot_union_rel : merge_union_rel (eqv_clot h) =2 eqv_clot h'.
proof: Proof. move => x y. rewrite /merge_union_rel /h' map_equivE. apply/idP/idP. - have aux z : merge_union_fwd (merge_union_bwd z) = z %[mod eqv_clot (map_pairs (@merge_union_fwd _ _ _) h)]. { apply/eqquotP. case: merge_union_bwdP => *; apply: eq_equiv; by apply: val_inj. } move => H. apply/eqquotP. rewrite -[_ x]aux -[_ y]aux. apply/eqquotP. move: H. apply: eqv_clot_map'. - rewrite eqv_clotE. apply: equiv_ofE => /= {x y} x y. rewrite /rel_of_pairs/=. case/mapP => /= [[u v]] in_h [-> ->]. apply/eqquotP. rewrite 2!(merge_union_can eqvI). apply/eqquotP. exact: eqv_clot_pair. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)