Swapping arguments in bumper forall.

Stream: Is there code for X?

[Wrenna Robson]

Do we have

theorem forall₂_comm
    {ι₁ ι₂ : Sort*} {κ₁ : ι₁ → Sort*} {κ₂ : ι₂ → Sort*} {p : ∀ i₁, κ₁ i₁ → ∀ i₂, κ₂ i₂ → Prop} :
    (∀ i₁ j₁ i₂ j₂, p i₁ j₁ i₂ j₂) ↔
    ∀ i₁ i₂, (j₁ : κ₁ i₁) → (j₂ : κ₂ i₂) → p i₁ j₁ i₂ j₂ := by simp_rw [forall_comm (α := ι₂)]

It is sort of a combination of forall₂_swap and forall_comm (hence the name I have given it here) but it seems like something that will so naturally come up that I can't quite believe it hasn't.