proposition: Lemma merge_disjoint_union_can' : cancel merge_union_bwd merge_union_fwd.
proof: Proof. move => x. case: merge_union_bwdP => //= {x} x *; exact: val_inj. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)