proposition: Lemma list_lookup_total_inserts `{!Inhabited A} l i k j : i ≤ j < i + length k → j < length l → list_inserts i k l !!! j = k !!! (j - i).
proof: Proof. intros. by rewrite !list_lookup_total_alt, list_lookup_inserts. Qed.
imports: stdpp(options)