proposition: Lemma natmap_omap_raw_wf {A B} (f : A → option B) l : natmap_wf l → natmap_wf (natmap_omap_raw f l).
proof: Proof. induction l; simpl; eauto using natmap_cons_canon_wf, natmap_wf_inv. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)