proposition: Lemma merge_union_bwdP x : merge_union_bwd_spec x (merge_union_bwd x).
proof: Proof. rewrite /merge_union_bwd. case: (setU_dec _) => p. - rewrite {1}[x](_ : x = Sub (val x) (valP x)). exact: merge_union_bwdL. by rewrite valK'. - rewrite {1}[x](_ : x = Sub (val x) (valP x)). apply: merge_union_bwdR. by rewrite p. by rewrite valK'. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries bij)