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