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