proposition: Lemma lookup_take_Some l n i a : take n l !! i = Some a ↔ l !! i = Some a ∧ i < n.
proof: Proof. split. - destruct (decide (i < n)). + rewrite lookup_take; naive_solver. + rewrite lookup_take_ge; [done|lia]. - intros [??]. by rewrite lookup_take. Qed.
imports: stdpp(options)