proposition: Lemma natmap_merge_wf {A B C} (f : option A → option B → option C) l1 l2 : natmap_wf l1 → natmap_wf l2 → natmap_wf (natmap_merge_raw f l1 l2).
proof: Proof. revert l2. induction l1; intros [|??]; simpl; eauto using natmap_omap_raw_wf, natmap_cons_canon_wf, natmap_wf_inv. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)