proposition: Lemma elem_of_lookup_zip_with l k (z : C) : z ∈ zip_with f l k ↔ ∃ i x y, z = f x y ∧ l !! i = Some x ∧ k !! i = Some y.
proof: Proof. naive_solver eauto using elem_of_lookup_zip_with_1, elem_of_lookup_zip_with_2. Qed.
imports: stdpp(options)