Graphs.hascasl.output revision bf089e1d4db3bf389ac1a352f4242e82c8f2b3c2
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
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) :
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, redeclared type 'S'
*** Hint 3.8, redeclared type 'Pred'
*** Hint 4.17, redeclared type 'S'
*** Hint 20.31, variable shadows global name(s) 'x'