∀(x : T) → x
