proposition: Lemma elem_of_lookup_zip_with_1 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. intros [i Hin]%elem_of_list_lookup. rewrite lookup_zip_with in Hin. simplify_option_eq; naive_solver. Qed.
imports: stdpp(options)