internal {type s, t; op o, q : s -> t;

. (op __=__ : forall a : Type . a � a ->? Unit) ((op o : s -> t),

(op q : s -> t))}

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

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

Unit : Type := Unit

s : Type

t : Type

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

__/\__ : Unit � Unit ->? Unit

__<=>__ : Unit � Unit ->? Unit

__=__ : forall a : Type . a � a ->? Unit

__=>__ : Unit � Unit ->? Unit

__=e=__ : forall a : Type . a � a ->? Unit

__\/__ : Unit � Unit ->? Unit

def__ : forall a : Type . a ->? Unit

if__then__else__ : forall a : Type . Unit � a � a ->? a

not__ : Unit ->? Unit

o : s -> t

q : s -> t

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

(op __=__ : forall a : Type . a � a ->? Unit) ((op o : s -> t),

(op q : s -> t)) %()%