∀(x : T) → ∀(y : U) → V