proposition: Lemma Exists_vlookup {A} (P : A → Prop) {n} (v : vec A n) : Exists P (vec_to_list v) ↔ ∃ i, P (v !!! i).
proof: Proof. rewrite Exists_exists. setoid_rewrite elem_of_vlookup. naive_solver. Qed.
imports: stdpp(countable) stdpp(options)