rel 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* R:(TTProp). 
Thm* (x,y:T. Dec(R(x,y)))
Thm* 
Thm* Linorder(T;x,y.R(x,y))  (a,b:T. strict_part(x,y.R(x,y);a;b)  R(b,a))		[linorder_lt_neg]
Thm* R:(TTProp). 
Thm* Linorder(T;x,y.R(x,y))  (a,b:T. R(a,b)  strict_part(x,y.R(x,y);b;a))		[linorder_le_neg]
Thm* R:(TTProp). 
Thm* (Trans a,b:T. R(a,b))
Thm* 
Thm* (a,b,c:T.
Thm* (strict_part(x,y.R(x,y);a;b)  R(b,c)  strict_part(x,y.R(x,y);a;c))		[trans_imp_sp_trans_b]
Thm* R:(TTProp). 
Thm* (Trans a,b:T. R(a,b))
Thm* 
Thm* (a,b,c:T.
Thm* (R(a,b)  strict_part(x,y.R(x,y);b;c)  strict_part(x,y.R(x,y);a;c))		[trans_imp_sp_trans_a]
Thm* R:(TTProp). 
Thm* (Trans a,b:T. R(a,b))  (Trans a,b:T. strict_part(x,y.R(x,y);a;b))		[trans_imp_sp_trans]
Thm* R:(TTProp). 
Thm* Order(T;x,y.R(x,y))
Thm* 
Thm* (x,y:T. Dec(x = y))
Thm* 
Thm* (a,b:T. R(a,b)  strict_part(x,y.R(x,y);a;b)  a = b)		[order_split]
Thm* R,R':(TTProp).
Thm* (x,y:T. R(x,y)  R'(x,y))
Thm* 
Thm* (Linorder(T;x,y.R(x,y))  Linorder(T;x,y.R'(x,y)))		[linorder_functionality_wrt_iff]
Thm* R,R':(TTProp).
Thm* (x,y:T. R(x,y)  R'(x,y))
Thm* 
Thm* (Order(T;x,y.R(x,y))  Order(T;x,y.R'(x,y)))		[order_functionality_wrt_iff]
Thm* R:(TTProp). 
Thm* (a,b:T. Dec(R(a,b)))
Thm* 
Thm* (Connex(T;x,y.R(x,y))
Thm* (
Thm* ((a,b:T.
Thm* ((strict_part(x,y.R(x,y);a;b)
Thm* (( Symmetrize(x,y.R(x,y);a;b)
Thm* (( strict_part(x,y.R(x,y);b;a)))		[connex_iff_trichot]
Thm* R,R':(TTProp).
Thm* (x,y:T. R(x,y)  R'(x,y))
Thm* 
Thm* Connex(T;x,y.R(x,y))  Connex(T;x,y.R'(x,y))		[connex_functionality_wrt_implies]
Thm* R,R':(TTProp).
Thm* (x,y:T. R(x,y)  R'(x,y))
Thm* 
Thm* (Connex(T;x,y.R(x,y))  Connex(T;x,y.R'(x,y)))		[connex_functionality_wrt_iff]
Thm* R:(TTProp), a,b:T. strict_part(x,y.R(x,y);a;b)  a = b[strict_part_irrefl]
Thm* R,R':(TTProp).
Thm* (x,y:T. R(x,y)  R'(x,y))
Thm* 
Thm* (AntiSym(T;x,y.R(x,y))  AntiSym(T;x,y.R'(x,y)))		[anti_sym_functionality_wrt_iff]
Thm* eq:(TT). SqStable(IsEqFun(T;eq))[sq_stable__eqfun_p]
Thm* E:(TTProp). (EquivRel x,y:T. E(x,y))  (EquivRel x,y:T. E(x,y))[squash_thru_equiv_rel]
Thm* R:(TTProp). 
Thm* (EquivRel x,y:T. R(x,y))
Thm* 
Thm* (a,a',b,b':T. R(a,b)  R(a',b')  (R(a,a')  R(b,b')))		[equiv_rel_self_functionality]
Thm* E:(TTProp), E':(T'T'Prop).
Thm* T = T'
Thm* 
Thm* (x,y:T. E(x,y)  E'(x,y))
Thm* 
Thm* ((EquivRel x,y:T. E(x,y))  (EquivRel x,y:T'. E'(x,y)))		[equiv_rel_functionality_wrt_iff]
Thm* R:(TTProp). 
Thm* (Trans x,y:T. R(x,y))
Thm* 
Thm* (a,a',b,b':T.
Thm* (Symmetrize(x,y.R(x,y);a;b)
Thm* (
Thm* (Symmetrize(x,y.R(x,y);a';b')  (R(a,a')  R(b,b')))		[trans_rel_func_wrt_sym_self]
Thm* R:(TTProp). 
Thm* Preorder(T;x,y.R(x,y))  (EquivRel a,b:T. Symmetrize(x,y.R(x,y);a;b))		[symmetrized_preorder]
Thm* R:(TTType), Q:(TProp).
Thm* (EquivRel x,y:T. R(x,y))  (EquivRel x,y:{z:T| Q(z) }. R(x,y))		[equiv_rel_subtyping]
Thm* R:(TTProp). 
Thm* (Trans x,y:T. R(x,y))
Thm* 
Thm* (a,a',b,b':T. R(b,a)  R(a',b')  R(a,a')  R(b,b'))		[trans_rel_self_functionality]
Thm* R,R':(TTProp).
Thm* (x,y:T. R(x,y)  R'(x,y))
Thm* 
Thm* ((Trans y,x:T. R(x,y))  (Trans y,x:T. R'(x,y)))		[trans_functionality_wrt_iff]
Thm* R,R':(TTProp).
Thm* (x,y:T. R(x,y)  R'(x,y))
Thm* 
Thm* ((Sym x,y:T. R(x,y))  (Sym x,y:T. R'(x,y)))		[sym_functionality_wrt_iff]
Thm* R,R':(TTProp).
Thm* (x,y:T. R(x,y)  R'(x,y))  (Refl(T;x,y.R(x,y))  Refl(T;x,y.R'(x,y)))		[refl_functionality_wrt_iff]
Def Irrefl(T;x,y.E(x;y)) == a:T. E(a;a)[irrefl]
Def Connex(T;x,y.R(x;y)) == x,y:T. R(x;y)  R(y;x)[connex]
Def StAntiSym(T;x,y.R(x;y)) == x,y:T. (R(x;y) & R(y;x))[st_anti_sym]
Def AntiSym(T;x,y.R(x;y)) == x,y:T. R(x;y)  R(y;x)  x = y[anti_sym]
Def IsEqFun(T;eq) == x,y:T. (x eq y)  x = y[eqfun_p]
Def Trans x,y:T. E(x;y) == a,b,c:T. E(a;b)  E(b;c)  E(a;c)[trans]
Def Sym x,y:T. E(x;y) == a,b:T. E(a;b)  E(b;a)[sym]
Def Refl(T;x,y.E(x;y)) == a:T. E(a;a)[refl]

In prior sections: core well fnd int 1 bool 1

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

rel 1 Sections StandardLIB Doc