proposition: Lemma elem_of_list_lookup_total `{!Inhabited A} l x : x ∈ l ↔ ∃ i, i < length l ∧ l !!! i = x.
proof: Proof. naive_solver eauto using elem_of_list_lookup_total_1, elem_of_list_lookup_total_2. Qed.
imports: stdpp(options)