type t

op f : ? t -> t

op g : t -> (? t)

op a, b : t

op c, d : ? t

. ((fun __=__[t] : forall a : Type . a * a ->? Unit) :

t * t ->? Unit)

((op f : ? t -> t)(op a : t) : t,

(op g : t -> ? t)(op c : ? t) : ? t) :

Unit

%% Type Constructors -----------------------------------------------------

? : +Type -> Type

Logical : Type := ? Unit

Pred : -Type -> Type := \ a : -Type . a ->? Unit

Unit : Type

__*__ : +Type -> +Type -> Type

__*__*__ : +Type -> +Type -> +Type -> Type

__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type

__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type

__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)

__-->?__ : -Type -> +Type -> Type < __->?__

__->__ : -Type -> +Type -> Type < __->?__

__->?__ : -Type -> +Type -> Type

t : Type

%% Assumptions -----------------------------------------------------------

__/\__ : ? Unit * ? Unit ->? Unit %(fun)%

__<=>__ : ? Unit * ? Unit ->? Unit %(fun)%

__=__ : forall a : Type . a * a ->? Unit %(fun)%

__=>__ : ? Unit * ? Unit ->? Unit %(fun)%

__=e=__ : forall a : Type . a * a ->? Unit %(fun)%

__\/__ : ? Unit * ? Unit ->? Unit %(fun)%

__if__ : ? Unit * ? Unit ->? Unit %(fun)%

__when__else__ : forall a : Type . a * ? Unit * a ->? a %(fun)%

a : t %(op)%

b : t %(op)%

bottom : forall a : Type . a %(fun)%

c : ? t %(op)%

d : ? t %(op)%

def__ : forall a : Type . a ->? Unit %(fun)%

f : ? t -> t %(op)%

false : Unit %(fun)%

g : t -> ? t %(op)%

not__ : ? Unit ->? Unit %(fun)%

true : Unit %(fun)%

�__ : ? Unit ->? Unit %(fun)%

%% Sentences -------------------------------------------------------------

(__=__ : t * t ->? Unit)(f(a) : t, g(c) : ? t) : Unit