proposition: Lemma merge_union_fwd_hom : {homo merge_union_fwd : x y / x = y %[mod e] >-> x = y %[mod merge_union_rel]}.
proof: Proof. move => x y H. apply/eqquotP. rewrite map_equivE. apply/eqquotP. by rewrite !merge_union_can. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)