English
Let eα, eβ, eγ be equivalences α₁ ≃ α₂, β₁ ≃ β₂, γ₁ ≃ γ₂. If h relates p x y z ↔ q (eα x) (eβ y) (eγ z), then (∀ x y z, p x y z) ↔ ∀ x y z, q x y z.
Русский
Пусть eα, eβ, eγ — эквивалентности между тройками. Если h связывает p x y z ↔ q (eα x) (eβ y) (eγ z), тогда (∀ x y z, p x y z) ↔ ∀ x y z, q x y z.
LaTeX
$$$ \forall eα:(\alpha _1 \simeq \alpha _2) (eβ:(\beta _1 \simeq \beta _2)) (eγ:(\gamma _1 \simeq \gamma _2),\ (\forall {x:\alpha _1} {y:\beta _1} {z:\gamma _1},\ p x y z \leftrightarrow q (eα x) (eβ y) (eγ z)) \rightarrow (\forall x y z, p x y z) \leftrightarrow (\forall x y z, q x y z) $$$
Lean4
protected theorem forall₃_congr {α₁ α₂ β₁ β₂ γ₁ γ₂ : Sort*} {p : α₁ → β₁ → γ₁ → Prop} {q : α₂ → β₂ → γ₂ → Prop}
(eα : α₁ ≃ α₂) (eβ : β₁ ≃ β₂) (eγ : γ₁ ≃ γ₂) (h : ∀ {x y z}, p x y z ↔ q (eα x) (eβ y) (eγ z)) :
(∀ x y z, p x y z) ↔ ∀ x y z, q x y z :=
Equiv.forall₂_congr _ _ <| Equiv.forall_congr _ <| @h _ _
