vars S, T : Type

types Bool;

Pred S := S ->? Unit;

Set S := S ->? Unit

ops True, False : Bool

ops emptySet : Set S;

{__} : S -> Set S;

__isIn__ : S * Set S ->? Unit;

__subset__ : Pred (Set (S) * Set (S));

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

__disjoint__ : Pred (Set (S) * Set (S));

__*__ : Set S * Set T -> Set (S * T);

__disjointUnion__ : Set S * Set S -> Set (S * Bool);

inl, inr : S -> S * Bool

forall x, x' : S; y : T; s, s' : Set S; t : Set T

. not x isIn emptySet

. x isIn { x' } <=> x = x'

. x isIn s <=> s x

. s subset s' <=> forall x : S . x isIn s => x isIn s'

. x isIn (s union s') <=> x isIn s \/ x isIn s'

. x isIn (s intersection s') <=> x isIn s /\ x isIn s'

. x isIn (s \\ s') <=> x isIn s /\ not x isIn s'

. s disjoint s' <=> s intersection s' = emptySet

. (x, y) isIn (s * t) <=> x isIn s /\ y isIn t

. inl x = (x, False)

. inr x = (x, True);

types

Bool : Type;

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

vars

S : Type %(var_1)%;

T : Type %(var_2)%

op False : Bool %(op)%

op True : Bool %(op)%

op __*__ : forall S : Type; T : Type . Set S * Set T -> Set (S * T)

%(op)%

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

op __disjoint__ : forall S : Type . Pred (Set S * Set S) %(op)%

op __disjointUnion__ : forall S : Type

. Set S * Set S -> Set (S * Bool)

%(op)%

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

%(op)%

op __isIn__ : forall S : Type . S * Set S ->? Unit %(op)%

op __subset__ : forall S : Type . Pred (Set S * Set S) %(op)%

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

op emptySet : forall S : Type . Set S %(op)%

op inl : forall S : Type . S -> S * Bool %(op)%

op inr : forall S : Type . S -> S * Bool %(op)%

op {__} : forall S : Type . S -> Set S %(op)%

vars

s : Set S;

s' : Set S;

t : Set T;

x : S;

x' : S;

y : T

. not x isIn emptySet

. x isIn { x' } <=> x = x'

. x isIn s <=> s x

. s subset s' <=> forall x : S . x isIn s => x isIn s'

. x isIn (s union s') <=> x isIn s \/ x isIn s'

. x isIn (s intersection s') <=> x isIn s /\ x isIn s'

. x isIn (s \\ s') <=> x isIn s /\ not x isIn s'

. s disjoint s' <=> s intersection s' = emptySet

. (x, y) isIn (s * t) <=> x isIn s /\ y isIn t

. inl x = (x, False)

. inr x = (x, True)

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

### Hint 1.8, is type variable 'T'

### Hint 3.19, rebound type variable 'S'

### Hint 3.8, redeclared type 'Pred'

### Hint 4.17, rebound type variable 'S'

### Hint 16.11, not a class 'S'

### Hint 16.14, not a class 'S'

### Hint 16.19, not a class 'T'

### Hint 16.24, not a kind 'Set (S)'

### Hint 16.27, not a kind 'Set (S)'

### Hint 16.37, not a kind 'Set (T)'

### Hint 20.32, not a class 'S'

### Hint 20.31, rebound variable 'x'