proposition: Lemma lookup_cons_Some x l i y : (x :: l) !! i = Some y ↔ (i = 0 ∧ x = y) ∨ (1 ≤ i ∧ l !! (i - 1) = Some y).
proof: Proof. rewrite lookup_cons. destruct i as [|i]. - naive_solver lia. - replace (S i - 1) with i by lia. naive_solver lia. Qed.
imports: stdpp(options)