var s : Type

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

type MyAlias : Type -> Type := \ t : Type . t_v2 ->? Unit

type a1 : Type -> Type -> Type := \ (a : Type)

(b : Type) . a_v3 -> b_v4 -> Unit

type a1 : Type -> Type -> Type := \ (a : Type)

(b : Type) . a_v5 -> b_v6 -> Unit

type a1 : Type -> Type -> Type := \ (a : Type)

(b : Type) . a_v7 -> b_v8 -> Unit

type a2 : Type -> Type -> Type := \ (a : Type)

(b : Type) . a_v9 -> Unit

type a3 : Type -> Type -> Type := \ (a : Type)

(a : Type) . a_v11 -> Unit

type a4 : Type -> Type -> Type := \ (a : Type)

(a : Type) . a_v12 -> Unit

type a5(a : Type)

type a5 : Type -> Type := \ a : Type . a5 a_v14 -> Unit

type a6(a : Type)

type a7 : Type -> Type := \ a : Type . a6 a_v16 -> Unit

type a6 : Type -> Type := \ a : Type . a7 a_v17 -> Unit

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

Logical : Type := Unit ->? Unit

MyAlias : Type -> Type := \ t : Type . t_v2 ->? Unit

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

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

Unit : Type := Unit

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

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

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

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

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

a1

: Type -> Type -> Type

:= \ (a : Type)(b : Type) . a_v3 -> b_v4 -> Unit

a2 : Type -> Type -> Type := \ (a : Type)(b : Type) . a_v9 -> Unit

a3 : Type -> Type -> Type := \ (a : Type)(a : Type) . a_v11 -> Unit

a4 : Type -> Type -> Type := \ (a : Type)(a : Type) . a_v12 -> Unit

a5 : Type -> Type

a6 : Type -> Type

a7 : Type -> Type := \ a : Type . a6 a_v16 -> Unit

s : Type %(var_1)%

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

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

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

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

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

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

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

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

__when__else__

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

bottom : forall a : Type . a_v-1 %(fun)%

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

false : Unit %(fun)%

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

true : Unit %(fun)%

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

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

*** Hint 1.5, is type variable 's'

*** Hint 6.6, redeclared type 'a1'

*** Hint 7.6, redeclared type 'a1'

*** Hint 11.19, redeclared type 'a'

*** Error 11.15, duplicates at '(11,19)' for 'a'

*** Error 13.9, duplicates at '(13,11)' for 'a'

*** Error 17.14, illegal recursive type synonym 'a5 a_v14 -> Unit'

*** Error 23.14, illegal recursive type synonym 'a7 a_v17 -> Unit'