var S : Type; N : Type; E : Type

type Set : Type -> Type := \ S : Type . S ->? Unit

type Graph : Type -> Type -> Type := \ (N : Type)

(E : Type) . (N ->? Unit) � (E ->? N) � (E ->? N)

op __union__ : forall E : Type; N : Type . ((N ->? Unit) �

(E ->? N) � (E ->? N)) �

((N ->? Unit) � (E ->? N) � (E ->? N)) -> (N ->? Unit) �

(E ->? N) �

(E ->? N);

__union__, __intersection__,

__\\__ : forall S : Type . (S ->? Unit) �

(S ->? Unit) -> S ->? Unit

forall g : (N ->? Unit) � (E ->? N) � (E ->? N);

g' : (N ->? Unit) � (E ->? N) � (E ->? N)

. (fun __=__ : forall a : Type . a �

a ->? Unit) ((op __union__ : forall E : Type;

N : Type . ((N ->? Unit) �

(E ->? N) �

(E ->? N)) �

((N ->? Unit) �

(E ->? N) �

(E ->? N)) -> (N ->? Unit) �

(E ->? N) �

(E ->? N)) ((var g : (N ->? Unit) �

(E ->? N) �

(E ->? N)),

(var g' : (N ->? Unit) �

(E ->? N) �

(E ->? N))),

(var g : (N ->? Unit) � (E ->? N) � (E ->? N)))

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

E : Type %(var)%

Graph : Type -> Type -> Type := \ (N : Type)

(E : Type) . (N ->? Unit) � (E ->? N) � (E ->? N)

N : Type %(var)%

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

S : Type %(var)%

Set : Type -> Type := \ S : Type . S ->? Unit

Unit : Type := Unit

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

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

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

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

__�__ : Type+ -> Type+ -> 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)%

__\\__ : forall S : Type . (S ->? Unit) �

(S ->? Unit) -> S ->? Unit %(Op)%

__if__ : Unit � Unit ->? Unit %(Fun)%

__intersection__ : forall S : Type . (S ->? Unit) �

(S ->? Unit) -> S ->? Unit %(Op)%

__union__ : forall S : Type . (S ->? Unit) �

(S ->? Unit) -> S ->? Unit %(Op)%

: forall E : Type; N : Type . ((N ->? Unit) � (E ->? N) �

(E ->? N)) �

((N ->? Unit) � (E ->? N) � (E ->? N)) -> (N ->? Unit) �

(E ->? N) �

(E ->? N) %(Op)%

__when__else__ : forall a : Type . a � Unit � a ->? a %(Fun)%

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

false : Unit %(Fun)%

if__then__else__ : forall a : Type . Unit � a � a ->? a %(Fun)%

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

true : Unit %(Fun)%

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

(fun __=__ : forall a : Type . a �

a ->? Unit) ((op __union__ : forall E : Type;

N : Type . ((N ->? Unit) �

(E ->? N) �

(E ->? N)) �

((N ->? Unit) �

(E ->? N) �

(E ->? N)) -> (N ->? Unit) �

(E ->? N) �

(E ->? N)) ((var g : (N ->? Unit) �

(E ->? N) �

(E ->? N)),

(var g' : (N ->? Unit) �

(E ->? N) �

(E ->? N))),

(var g : (N ->? Unit) � (E ->? N) � (E ->? N))) %()%

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

*** Hint 1.7, is type variable 'S'

*** Hint 1.9, is type variable 'N'

*** Hint 1.11, is type variable 'E'

*** Hint 9.6, no type match for: g

with type: '_var_6 ->? Unit' (line 2, column 19)

known types:

'(N ->? Unit) � (E ->? N) � (E ->? N)'