Graphs.hascasl.output revision c2dead95fafd7ca36d06ddf07606a1292ead6d8a
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 -----------------------------------------------------
Bool : Type
Logical : Type := Unit ->? 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.18, 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'