proposition: Lemma list_lookup_alt `{!Inhabited A} l i x : l !! i = Some x ↔ i < length l ∧ l !!! i = x.
proof: Proof. naive_solver eauto using list_lookup_lookup_total_lt, list_lookup_total_correct, lookup_lt_Some. Qed.
imports: stdpp(options)