proposition: Lemma natmap_partial_alter_wf {A} (f : option A → option A) i l : natmap_wf l → natmap_wf (natmap_partial_alter_raw f i l).
proof: Proof. revert i. induction l; [intro | intros [|?]]; simpl; repeat case_match; eauto using natmap_singleton_wf, natmap_cons_canon_wf, natmap_wf_inv. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)