proposition: Lemma elem_of_lookup_zip_with_2 l k x y (z : C) i : l !! i = Some x → k !! i = Some y → f x y ∈ zip_with f l k.
proof: Proof. intros Hl Hk. rewrite elem_of_list_lookup. exists i. by rewrite lookup_zip_with, Hl, Hk. Qed.
imports: stdpp(options)