proposition: Lemma lookup_zip_with_Some l k i z : zip_with f l k !! i = Some z ↔ ∃ x y, z = f x y ∧ l !! i = Some x ∧ k !! i = Some y.
proof: Proof. rewrite lookup_zip_with. destruct (l !! i), (k !! i); naive_solver. Qed.
imports: stdpp(options)