class Cpo < Type

class Cppo < Cpo

type instance __-->__ : -Cpo -> +Cpo -> Cpo

type instance __-->__ : -Cpo -> +Cppo -> Cppo

var c : Cppo

fun Y : (c --> c) --> c

%% Classes ---------------------------------------------------------------

Cpo < Type

Cppo < Cpo

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

__-->__

: (-Cpo -> +Cppo -> Cppo, -Cpo -> +Cpo -> Cpo,

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

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

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

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

%% Type Variables --------------------------------------------------------

c : Cppo %(var_1)%

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

Y : forall c : Cppo . (c --> c) --> c %(fun)%

__/\__ : ? 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)%

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

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

false : Unit %(fun)%

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

true : Unit %(fun)%

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

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

### Hint 8.5, is type variable 'c'