proposition: Lemma lookup_replicate n x y i : replicate n x !! i = Some y ↔ y = x ∧ i < n.
proof: Proof. split. - revert i. induction n; intros [|?]; naive_solver auto with lia. - intros [-> Hi]. revert i Hi. induction n; intros [|?]; naive_solver auto with lia. Qed.
imports: stdpp(options)