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