∀ A, (A → ℙ) → ℙ

Parameter ex : forall (A:Type), (A -> Prop) -> Prop

axiom ex : \forall A : Type[0] . (A -> Prop) -> Prop

constant ex : forall (A : Type) , ((A) -> Prop) -> Prop

sttfa_ex [A:TYPE+] : [[A -> bool] -> bool]

Printing for OpenTheory is not working at the moment.