var s : Type

type MyPred : Type := \ s : Type . s ->? Unit

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

MyPred : Type := \ s : Type . s ->? Unit

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

Unit : Type := Unit

s : Type %(var)%

%% 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

%% Diagnostics -----------------------------------------------------------

Hint (line 1, column 5) is type variable 's'