Forall₂ trans ish

public theorem forall₂_trans_ish {xs : List α} {ys : List β} {zs : List γ} {Q : α → β → Prop} {R : α → γ → Prop} {S : β → γ → Prop}  (h₁ : List.Forall₂ Q xs ys)  (h₂ : List.Forall₂ R xs zs) :  (∀ {a b c}, Q a b → R a c → S b c) →  List.Forall₂ S ys zs:= by  intro h  induction h₁ generalizing zs with  | nil => simp [forall₂_nil_left_iff] at h₂ ; simp [h₂]  | cons hhd₁ htl₁ ih =>    rename_i xhd yhd xtl ytl    cases h₂ with    | cons hhd₂ htl₂ =>      rename_i zhd ztl      specialize @ih ztl      apply Forall₂.cons      · exact h hhd₁ hhd₂      · exact ih htl₂