proposition: Lemma lookup_app l1 l2 i : (l1 ++ l2) !! i = match l1 !! i with Some x => Some x | None => l2 !! (i - length l1) end.
proof: Proof. revert i. induction l1 as [|x l1 IH]; intros [|i]; naive_solver. Qed.
imports: stdpp(options)