∀(x : T) -> y