∀(x : T) → x