proposition: Lemma elem_of_list_lookup_total_1 `{!Inhabited A} l x : x ∈ l → ∃ i, i < length l ∧ l !!! i = x.
proof: Proof. intros [i Hi]%elem_of_list_lookup_1. eauto using lookup_lt_Some, list_lookup_total_correct. Qed.
imports: stdpp(options)