Graphs.hascasl.output revision d48085f765fca838c1d972d2123601997174583d
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) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S,
(op emptySet[S] : forall S : Type . (Set S_v-1)@(S_v-1 ->? Unit)) :
(Set S)@(S ->? Unit)) :
Unit) :
Unit
. (fun __<=>__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S,
((op {__}[S]
: forall S : Type . S_v-1 -> (Set S_v-1)@(S_v-1 ->? Unit)) :
S -> (Set S)@(S ->? Unit))
(var x' : S) :
(Set S)@(S ->? Unit)) :
Unit,
((fun __=__[S] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
S * S ->? Unit)
(var x : S, var x' : S) :
Unit) :
Unit
. (fun __<=>__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s : (Set S)@(S ->? Unit)) :
Unit,
(var s : (Set S)@(S ->? Unit))(var x : S) : Unit) :
Unit
. (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)) :
(Pred (Set S * Set S))@((Set S)@(S ->? Unit) * (Set S)@(S ->? Unit)
->? Unit))
(var s : (Set S)@(S ->? Unit), var s' : (Set S)@(S ->? Unit)) :
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) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s : (Set S)@(S ->? Unit)) :
Unit,
((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s' : (Set S)@(S ->? Unit)) :
Unit) :
Unit) :
Unit
. (fun __<=>__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? 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)) :
(Set S)@(S ->? Unit) * (Set S)@(S ->? Unit) ->
(Set S)@(S ->? Unit))
(var s : (Set S)@(S ->? Unit), var s' : (Set S)@(S ->? Unit)) :
(Set S)@(S ->? Unit)) :
Unit,
(fun __\/__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s : (Set S)@(S ->? Unit)) :
Unit,
((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s' : (Set S)@(S ->? Unit)) :
Unit) :
Unit) :
Unit
. (fun __<=>__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? 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)) :
(Set S)@(S ->? Unit) * (Set S)@(S ->? Unit) ->
(Set S)@(S ->? Unit))
(var s : (Set S)@(S ->? Unit), var s' : (Set S)@(S ->? Unit)) :
(Set S)@(S ->? Unit)) :
Unit,
(fun __/\__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s : (Set S)@(S ->? Unit)) :
Unit,
((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s' : (Set S)@(S ->? Unit)) :
Unit) :
Unit) :
Unit
. (fun __<=>__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? 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)) :
(Set S)@(S ->? Unit) * (Set S)@(S ->? Unit) ->
(Set S)@(S ->? Unit))
(var s : (Set S)@(S ->? Unit), var s' : (Set S)@(S ->? Unit)) :
(Set S)@(S ->? Unit)) :
Unit,
(fun __/\__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s : (Set S)@(S ->? Unit)) :
Unit,
(fun not__ : ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s' : (Set S)@(S ->? Unit)) :
Unit) :
Unit) :
Unit) :
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)) :
(Pred (Set S * Set S))@((Set S)@(S ->? Unit) * (Set S)@(S ->? Unit)
->? Unit))
(var s : (Set S)@(S ->? Unit), var s' : (Set S)@(S ->? Unit)) :
Unit,
((fun __=__[S ->? Unit]
: forall a : Type . a_v-1 * a_v-1 ->? Unit) :
(S ->? Unit) * (S ->? Unit) ->? 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)) :
(Set S)@(S ->? Unit) * (Set S)@(S ->? Unit) ->
(Set S)@(S ->? Unit))
(var s : (Set S)@(S ->? Unit), var s' : (Set S)@(S ->? Unit)) :
(Set S)@(S ->? Unit),
(op emptySet[S] : forall S : Type . (Set S_v-1)@(S_v-1 ->? Unit)) :
(Set S)@(S ->? Unit)) :
Unit) :
Unit
. (fun __<=>__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S * T]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
(S * T) * (Set (S * T))@(S * T ->? 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)) :
(Set S)@(S ->? Unit) * (Set T)@(T ->? Unit) ->
(Set (S * T))@(S * T ->? Unit))
(var s : (Set S)@(S ->? Unit), var t : (Set T)@(T ->? Unit)) :
(Set (S * T))@(S * T ->? Unit)) :
Unit,
(fun __/\__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s : (Set S)@(S ->? Unit)) :
Unit,
((op __isIn__[T]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
T * (Set T)@(T ->? Unit) ->? Unit)
(var y : T, var t : (Set T)@(T ->? Unit)) :
Unit) :
Unit) :
Unit
. ((fun __=__[S * Bool]
: forall a : Type . a_v-1 * a_v-1 ->? Unit) :
(S * Bool) * (S * Bool) ->? Unit)
(((op inl[S] : forall S : Type . S_v-1 -> S_v-1 * Bool) :
S -> S * Bool)
(var x : S) :
S * Bool,
(var x : S, op False : Bool)) :
Unit
. ((fun __=__[S * Bool]
: forall a : Type . a_v-1 * a_v-1 ->? Unit) :
(S * Bool) * (S * Bool) ->? Unit)
(((op inr[S] : forall S : Type . S_v-1 -> S_v-1 * Bool) :
S -> S * Bool)
(var x : S) :
S * Bool,
(var x : S, op True : Bool)) :
Unit
%% Type Constructors -----------------------------------------------------
? : +Type -> Type
Bool : Type
Logical : Type := ? Unit
Pred : -Type -> Type := \ a : -Type . a_v-1 ->? Unit
Set : Type -> Type := \ S : Type . S_v-1 ->? Unit
Unit : Type
__*__ : +Type -> +Type -> Type
__*__*__ : +Type -> +Type -> +Type -> Type
__*__*__*__ : +Type -> +Type -> +Type -> +Type -> Type
__*__*__*__*__ : +Type -> +Type -> +Type -> +Type -> +Type -> Type
__-->__ : -Type -> +Type -> Type < (__-->?__, __->__)
__-->?__ : -Type -> +Type -> Type < __->?__
__->__ : -Type -> +Type -> Type < __->?__
__->?__ : -Type -> +Type -> Type
%% Type Variables --------------------------------------------------------
S : Type %(var_1)%
T : Type %(var_2)%
%% 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)%
%% Variables -------------------------------------------------------------
s : (Set S)@(S ->? Unit)
s' : (Set S)@(S ->? Unit)
t : (Set T)@(T ->? Unit)
x : S
x' : S
y : T
%% Sentences -------------------------------------------------------------
(fun not__ : ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S,
(op emptySet[S] : forall S : Type . (Set S_v-1)@(S_v-1 ->? Unit)) :
(Set S)@(S ->? Unit)) :
Unit) :
Unit
(fun __<=>__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S,
((op {__}[S]
: forall S : Type . S_v-1 -> (Set S_v-1)@(S_v-1 ->? Unit)) :
S -> (Set S)@(S ->? Unit))
(var x' : S) :
(Set S)@(S ->? Unit)) :
Unit,
((fun __=__[S] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
S * S ->? Unit)
(var x : S, var x' : S) :
Unit) :
Unit
(fun __<=>__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s : (Set S)@(S ->? Unit)) :
Unit,
(var s : (Set S)@(S ->? Unit))(var x : S) : Unit) :
Unit
(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)) :
(Pred (Set S * Set S))@((Set S)@(S ->? Unit) * (Set S)@(S ->? Unit)
->? Unit))
(var s : (Set S)@(S ->? Unit), var s' : (Set S)@(S ->? Unit)) :
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) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s : (Set S)@(S ->? Unit)) :
Unit,
((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s' : (Set S)@(S ->? Unit)) :
Unit) :
Unit) :
Unit
(fun __<=>__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? 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)) :
(Set S)@(S ->? Unit) * (Set S)@(S ->? Unit) ->
(Set S)@(S ->? Unit))
(var s : (Set S)@(S ->? Unit), var s' : (Set S)@(S ->? Unit)) :
(Set S)@(S ->? Unit)) :
Unit,
(fun __\/__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s : (Set S)@(S ->? Unit)) :
Unit,
((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s' : (Set S)@(S ->? Unit)) :
Unit) :
Unit) :
Unit
(fun __<=>__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? 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)) :
(Set S)@(S ->? Unit) * (Set S)@(S ->? Unit) ->
(Set S)@(S ->? Unit))
(var s : (Set S)@(S ->? Unit), var s' : (Set S)@(S ->? Unit)) :
(Set S)@(S ->? Unit)) :
Unit,
(fun __/\__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s : (Set S)@(S ->? Unit)) :
Unit,
((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s' : (Set S)@(S ->? Unit)) :
Unit) :
Unit) :
Unit
(fun __<=>__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? 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)) :
(Set S)@(S ->? Unit) * (Set S)@(S ->? Unit) ->
(Set S)@(S ->? Unit))
(var s : (Set S)@(S ->? Unit), var s' : (Set S)@(S ->? Unit)) :
(Set S)@(S ->? Unit)) :
Unit,
(fun __/\__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s : (Set S)@(S ->? Unit)) :
Unit,
(fun not__ : ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s' : (Set S)@(S ->? Unit)) :
Unit) :
Unit) :
Unit) :
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)) :
(Pred (Set S * Set S))@((Set S)@(S ->? Unit) * (Set S)@(S ->? Unit)
->? Unit))
(var s : (Set S)@(S ->? Unit), var s' : (Set S)@(S ->? Unit)) :
Unit,
((fun __=__[S ->? Unit]
: forall a : Type . a_v-1 * a_v-1 ->? Unit) :
(S ->? Unit) * (S ->? Unit) ->? 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)) :
(Set S)@(S ->? Unit) * (Set S)@(S ->? Unit) ->
(Set S)@(S ->? Unit))
(var s : (Set S)@(S ->? Unit), var s' : (Set S)@(S ->? Unit)) :
(Set S)@(S ->? Unit),
(op emptySet[S] : forall S : Type . (Set S_v-1)@(S_v-1 ->? Unit)) :
(Set S)@(S ->? Unit)) :
Unit) :
Unit
(fun __<=>__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S * T]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
(S * T) * (Set (S * T))@(S * T ->? 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)) :
(Set S)@(S ->? Unit) * (Set T)@(T ->? Unit) ->
(Set (S * T))@(S * T ->? Unit))
(var s : (Set S)@(S ->? Unit), var t : (Set T)@(T ->? Unit)) :
(Set (S * T))@(S * T ->? Unit)) :
Unit,
(fun __/\__ : ? Unit * ? Unit ->? Unit)
(((op __isIn__[S]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
S * (Set S)@(S ->? Unit) ->? Unit)
(var x : S, var s : (Set S)@(S ->? Unit)) :
Unit,
((op __isIn__[T]
: forall S : Type .
S_v-1 * (Set S_v-1)@(S_v-1 ->? Unit) ->? Unit) :
T * (Set T)@(T ->? Unit) ->? Unit)
(var y : T, var t : (Set T)@(T ->? Unit)) :
Unit) :
Unit) :
Unit
((fun __=__[S * Bool] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
(S * Bool) * (S * Bool) ->? Unit)
(((op inl[S] : forall S : Type . S_v-1 -> S_v-1 * Bool) :
S -> S * Bool)
(var x : S) :
S * Bool,
(var x : S, op False : Bool)) :
Unit
((fun __=__[S * Bool] : forall a : Type . a_v-1 * a_v-1 ->? Unit) :
(S * Bool) * (S * Bool) ->? Unit)
(((op inr[S] : forall S : Type . S_v-1 -> S_v-1 * Bool) :
S -> S * Bool)
(var x : S) :
S * Bool,
(var x : S, op True : Bool)) :
Unit
%% Diagnostics -----------------------------------------------------------
*** 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'