vars S, N, E : Type

type Set S := S ->? Unit

type Graph N E := Set N * (E ->? N) * (E ->? N)

ops __union__ : Graph N E * Graph N E -> Graph N E;

__union__, __intersection__, __\\__ : Set S * Set S -> Set S

forall g, g' : Graph N E . g union g' = g;

types

Graph : Type -> Type -> Type := \ N : Type . _t7;

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

_t7 : Type -> Type := \ E : Type . Set N * (E ->? N) * (E ->? N)

vars

E : Type %(var_3)%;

N : Type %(var_2)%;

S : Type %(var_1)%

op __\\__ : forall S : Type . Set S * Set S -> Set S %(op)%

op __intersection__ : forall S : Type . Set S * Set S -> Set S

%(op)%

op __union__ : forall S : Type . Set S * Set S -> Set S %(op)%

op __union__ : forall N : Type; E : Type

. Graph N E * Graph N E -> Graph N E

%(op)%

vars

g : Graph N E;

g' : Graph N E

. (__union__ : Graph N E * Graph N E -> Graph N E) (g, g') = g

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

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

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

### Hint 8.11, not a kind 'Graph N E'

### Hint 8.15, not a kind 'Graph N E'

### Hint 9.6-9.14, in type of '((var g : Graph N E), (var g' : Graph N E))'

type 'Graph N' (8.23)

is not unifiable with type 'Set' (6.47)

### Hint 9.6-9.14, untypable term (with type: Set _v16_S * Set _v16_S)

'(g, g')'