proposition: Lemma lookup_app_Some l1 l2 i x : (l1 ++ l2) !! i = Some x ↔ l1 !! i = Some x ∨ length l1 ≤ i ∧ l2 !! (i - length l1) = Some x.
proof: Proof. rewrite lookup_app. destruct (l1 !! i) eqn:Hi. - apply lookup_lt_Some in Hi. naive_solver lia. - apply lookup_ge_None in Hi. naive_solver lia. Qed.
imports: stdpp(options)