. __=__ = __<=>__

. true = ();

vars p, q : Logical

. p /\ q = p res q

. (p => q) = ((\ . p) =e= \ . p /\ q)

. (p <=> q) = ((p => q) /\ (q => p));

vars t : Type; pr : Pred t

. (forall y : t . pr y) = ((\ y : t . pr y) =e= \ y : t . true)

. false = forall a : Logical . a ()

. not p <=> p => false

. p \/ q

<=> forall a : Logical . (p => a ()) /\ (q => a ()) => a ()

. (exists y : t . pr y)

= forall a : Logical . (forall y : t . pr y => a ()) => a ();

vars a, b : t

. a = b <=> (def a => a =e= b) /\ (def b => def a);

op choose : Pred t ->? t

. choose pr = a <=> forall y : t . pr y <=> a = y;

op epsilon : Pred t -> t

. (exists x : t . pr x) => pr (epsilon pr)

. p \/ not p; %implied

var

t : Type %(var_18)%

op choose : forall t : Type . Pred t ->? t

op epsilon : forall t : Type . Pred t -> t

vars

a : t;

b : t;

p : Logical;

pr : Pred t;

q : Logical

. __=__ = __<=>__

. true = ()

forall p : Logical; q : Logical . p /\ q = p res q

forall p : Logical; q : Logical

. (p => q) = ((\ . p) =e= \ . p /\ q)

forall p : Logical; q : Logical

. (p <=> q) = ((p => q) /\ (q => p))

forall t : Type; pr : Pred t

. (forall y : t . pr y) = ((\ y : t . pr y) =e= \ y : t . true)

. false = forall a : Logical . a ()

forall p : Logical . not p <=> p => false

forall p : Logical; q : Logical

. p \/ q

<=> forall a : Logical . (p => a ()) /\ (q => a ()) => a ()

forall t : Type; pr : Pred t

. (exists y : t . pr y)

= forall a : Logical . (forall y : t . pr y => a ()) => a ()

forall t : Type; a : t; b : t

. a = b <=> (def a => a =e= b) /\ (def b => def a)

forall t : Type; a : t; pr : Pred t

. choose pr = a <=> forall y : t . pr y <=> a = y

forall t : Type; pr : Pred t

. (exists x : t . pr x) => pr (epsilon pr)

forall p : Logical . p \/ not p %implied

4.7: ### Hint: not a class 'Logical'

4.10: ### Hint: not a class 'Logical'

11.6: ### Hint: is type variable 't'

11.19: ### Hint: not a kind 'Pred t'

12.13: ### Hint: not a class 't'

14.20: ### Hint: not a class 'Logical'

18.23: ### Hint: not a class 'Logical'

20.13: ### Hint: not a class 't'

20.36: ### Hint: not a class 'Logical'

21.16: ### Hint: not a class 't'

23.7: ### Hint: not a class 't'

23.10: ### Hint: not a class 't'

27.30: ### Hint: not a class 't'

30.13: ### Hint: not a class 't'