Forall₂ implies all left

public theorem forall₂_implies_all_left {α β} {R : α → β → Prop} {xs : List α} {ys : List β} :  List.Forall₂ R xs ys →  ∀ x ∈ xs, ∃ y ∈ ys, R x y:= by  intro h  induction h  case nil =>    simp only [not_mem_nil, false_and, exists_false, imp_self, implies_true]  case cons xhd yhd xtl ytl hhd _ ih =>    intro x hx    simp only [mem_cons] at hx    rcases hx with hx | hx    · subst hx      exists yhd      simp only [mem_cons, true_or, hhd, and_self]    · have ⟨y, ih⟩ := ih x hx      exists y      simp only [mem_cons, ih, or_true, and_self]