proposition: Lemma merge_disjoint_union_can : cancel merge_union_fwd merge_union_bwd.
proof: Proof. move => [x|x] /=. - by rewrite merge_union_bwdEl // valK'. - by rewrite merge_union_bwdEr ?valK' // (disjointFl disUV). Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)