var a : Type

pred phi : a

. (forall x : a . phi x) = ((\ x : a . phi x) =e= \ x : a . ());

var p : Logical

. p \/ not p;

var

a : Type %(var_1)%

op phi : forall a : Type . a ->? Unit %(pred)%

var

p : Logical

forall a : Type

. (forall x : a . phi x) = ((\ x : a . phi x) =e= \ x : a . ())

forall p : Logical . p \/ not p

### Hint 3.12, not a class 'a'

### Hint 5.7, not a class 'Logical'