proposition: Lemma natmap_fmap_wf {A B} (f : A → B) l : natmap_wf l → natmap_wf (natmap_fmap_raw f l).
proof: Proof. unfold natmap_fmap_raw, natmap_wf. rewrite fmap_last. destruct (last l); [|done]. by apply fmap_is_Some. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)