proposition: Lemma lookup_snoc_Some x l i y : (l ++ [x]) !! i = Some y ↔ (i < length l ∧ l !! i = Some y) ∨ (i = length l ∧ x = y).
proof: Proof. rewrite lookup_app_Some, list_lookup_singleton_Some. naive_solver auto using lookup_lt_is_Some_1 with lia. Qed.
imports: stdpp(options)