proposition: Lemma merge_union_can' x : merge_union_fwd (merge_union_bwd x) = x %[mod merge_union_rel].
proof: Proof. case: merge_union_bwdP => {x} *; congr pi; exact: val_inj. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)