proposition: Lemma natmap_lookup_fmap_raw {A B} (f : A → B) i l : mjoin (natmap_fmap_raw f l !! i) = f <$> mjoin (l !! i).
proof: Proof. unfold natmap_fmap_raw. rewrite list_lookup_fmap. by destruct (l !! i). Qed.
imports: stdpp(fin_maps mapset) stdpp(options)