∀(x : A) → x