var S : Type; T : Type

type Bool; Pred : Type -> Type := \ S : Type . S_v-1 ->? Unit;

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

op True, False : Bool

op 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 : S; x' : S; y : T; s : Set S@(S ->? Unit);

s' : Set S@(S ->? Unit); t : Set T@(T ->? Unit)

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S,

op emptySet[S] : forall S : Type . Set S_v-1@(S_v-1 ->? Unit)))

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S,

(op {__}[S]

: forall S : Type . S_v-1 -> Set S_v-1@(S_v-1 ->? Unit))

(var x' : S)),

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

(var x : S, var x' : S))

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s : Set S@(S ->? Unit)),

(var s : Set S@(S ->? Unit))(var x : S))

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

((op __subset__[S]

: forall S : Type .

Pred (Set S_v-1 * Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit))

(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit)),

forall x : S

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s : Set S@(S ->? Unit)),

(op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s' : Set S@(S ->? Unit))))

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S,

(op __union__[S]

: forall S : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit))

(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit))),

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s : Set S@(S ->? Unit)),

(op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s' : Set S@(S ->? Unit))))

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S,

(op __intersection__[S]

: forall S : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit))

(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit))),

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s : Set S@(S ->? Unit)),

(op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s' : Set S@(S ->? Unit))))

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S,

(op __\\__[S]

: forall S : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit))

(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit))),

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s : Set S@(S ->? Unit)),

(fun not__ : ? Unit ->? Unit)

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s' : Set S@(S ->? Unit)))))

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

((op __disjoint__[S]

: forall S : Type .

Pred (Set S_v-1 * Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit))

(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit)),

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

((op __intersection__[S]

: forall S : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit))

(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit)),

op emptySet[S] : forall S : Type . Set S_v-1@(S_v-1 ->? Unit)))

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

((op __isIn__[S * T]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

((var x : S, var y : T),

(op __*__[S; T]

: forall S : Type; T : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set T_v-2@(T_v-2 ->? Unit) -> Set (S_v-1 * T_v-2)@(S_v-1 *

T_v-2 ->? Unit))

(var s : Set S@(S ->? Unit), var t : Set T@(T ->? Unit))),

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s : Set S@(S ->? Unit)),

(op __isIn__[T]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var y : T, var t : Set T@(T ->? Unit))))

. (fun __=__[S * Bool] : forall a : Type . a_v-1 * a_v-1 ->? Unit)

((op inl[S] : forall S : Type . S_v-1 -> S_v-1 * Bool)(var x : S),

(var x : S, op False : Bool))

. (fun __=__[S * Bool] : forall a : Type . a_v-1 * a_v-1 ->? Unit)

((op inr[S] : forall S : Type . S_v-1 -> S_v-1 * Bool)(var x : S),

(var x : S, op True : Bool))

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

Bool : Type

Logical : Type := Unit ->? Unit

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

S : Type %(var_1)%

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

T : Type %(var_2)%

Unit : Type

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

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

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

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

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

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

False : Bool %(op)%

True : Bool %(op)%

__*__

: forall S : Type; T : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set T_v-2@(T_v-2 ->? Unit) -> Set (S_v-1 * T_v-2)@(S_v-1 *

T_v-2 ->? Unit)

%(op)%

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

__\\__

: forall S : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit)

%(op)%

__disjoint__

: forall S : Type .

Pred (Set S_v-1 * Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

%(op)%

__disjointUnion__

: forall S : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) -> Set (S_v-1 * Bool)@(S_v-1 *

Bool ->? Unit)

%(op)%

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

__intersection__

: forall S : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit)

%(op)%

__isIn__

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit

%(op)%

__subset__

: forall S : Type .

Pred (Set S_v-1 * Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

%(op)%

__union__

: forall S : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit)

%(op)%

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

emptySet : forall S : Type . Set S_v-1@(S_v-1 ->? Unit) %(op)%

false : Unit %(fun)%

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

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

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

true : Unit %(fun)%

{__} : forall S : Type . S_v-1 -> Set S_v-1@(S_v-1 ->? Unit) %(op)%

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

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

(fun not__ : ? Unit ->? Unit)

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S,

op emptySet[S] : forall S : Type . Set S_v-1@(S_v-1 ->? Unit)))

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S,

(op {__}[S]

: forall S : Type . S_v-1 -> Set S_v-1@(S_v-1 ->? Unit))

(var x' : S)),

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

(var x : S, var x' : S))

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s : Set S@(S ->? Unit)),

(var s : Set S@(S ->? Unit))(var x : S))

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

((op __subset__[S]

: forall S : Type .

Pred (Set S_v-1 * Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit))

(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit)),

forall x : S

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s : Set S@(S ->? Unit)),

(op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s' : Set S@(S ->? Unit))))

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S,

(op __union__[S]

: forall S : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit))

(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit))),

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s : Set S@(S ->? Unit)),

(op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s' : Set S@(S ->? Unit))))

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S,

(op __intersection__[S]

: forall S : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit))

(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit))),

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s : Set S@(S ->? Unit)),

(op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s' : Set S@(S ->? Unit))))

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S,

(op __\\__[S]

: forall S : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit))

(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit))),

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s : Set S@(S ->? Unit)),

(fun not__ : ? Unit ->? Unit)

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s' : Set S@(S ->? Unit)))))

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

((op __disjoint__[S]

: forall S : Type .

Pred (Set S_v-1 * Set S_v-1)@(Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) ->? Unit))

(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit)),

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

((op __intersection__[S]

: forall S : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set S_v-1@(S_v-1 ->? Unit) -> Set S_v-1@(S_v-1 ->? Unit))

(var s : Set S@(S ->? Unit), var s' : Set S@(S ->? Unit)),

op emptySet[S] : forall S : Type . Set S_v-1@(S_v-1 ->? Unit)))

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

((op __isIn__[S * T]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

((var x : S, var y : T),

(op __*__[S; T]

: forall S : Type; T : Type .

Set S_v-1@(S_v-1 ->? Unit) *

Set T_v-2@(T_v-2 ->? Unit) -> Set (S_v-1 * T_v-2)@(S_v-1 *

T_v-2 ->? Unit))

(var s : Set S@(S ->? Unit), var t : Set T@(T ->? Unit))),

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

((op __isIn__[S]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var x : S, var s : Set S@(S ->? Unit)),

(op __isIn__[T]

: forall S : Type . S_v-1 * Set S_v-1@(S_v-1 ->? Unit) ->? Unit)

(var y : T, var t : Set T@(T ->? Unit))))

(fun __=__[S * Bool] : forall a : Type . a_v-1 * a_v-1 ->? Unit)

((op inl[S] : forall S : Type . S_v-1 -> S_v-1 * Bool)(var x : S),

(var x : S, op False : Bool))

(fun __=__[S * Bool] : forall a : Type . a_v-1 * a_v-1 ->? Unit)

((op inr[S] : forall S : Type . S_v-1 -> S_v-1 * Bool)(var x : S),

(var x : S, op True : Bool))

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

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

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

*** Hint 3.18, redeclared type 'S'

*** Hint 3.8, redeclared type 'Pred'

*** Hint 4.17, redeclared type 'S'

*** Warning 20.31, variable shadows global name(s) 'x'