Add lemma `lookup_total_fmap`.

stdpp/fin_maps.v

@@ -722,6 +722,10 @@ Proof.
   apply (inj (fmap (M:=option) f)). by rewrite <-!lookup_fmap, Hm.
 Qed.
 
+Lemma lookup_total_fmap `{!Inhabited A, !Inhabited B} (f : A → B) (m : M A) i :
+  is_Some (m !! i) → (f <$> m) !!! i = f (m !!! i).
+Proof. rewrite !lookup_total_alt, lookup_fmap. by intros [? ->]. Qed.
+
 Lemma lookup_fmap_Some {A B} (f : A → B) (m : M A) i y :
   (f <$> m) !! i = Some y ↔ ∃ x, f x = y ∧ m !! i = Some x.
 Proof. rewrite lookup_fmap, fmap_Some. naive_solver. Qed.