proposition: Lemma natmap_lookup_partial_alter_raw {A} (f : option A → option A) i l : mjoin (natmap_partial_alter_raw f i l !! i) = f (mjoin (l !! i)).
proof: Proof. revert i. induction l; intros [|?]; simpl; repeat case_match; simpl; autorewrite with natmap; auto. Qed.
imports: stdpp(fin_maps mapset) stdpp(options)