proposition: Lemma list_lookup_total_fmap `{!Inhabited A, !Inhabited B} l i : i < length l → (f <$> l) !!! i = f (l !!! i).
proof: Proof. intros [x Hx]%lookup_lt_is_Some_2. by rewrite !list_lookup_total_alt, list_lookup_fmap, Hx. Qed.
imports: stdpp(options)