Def  x:A. B(x) == x:AB(x)

is mentioned by

Thm*  e:(BB).  Thm*  (b:B. e(b) = b) Thm*   Thm*  (A:Type, f:(AAB). (a:A. (Diag f wrt x. e(x)) = f(a)))	[diagonalization_wrt_eq]
Thm*  R:(BBProp), e:(BB). Thm*  (b:B. R(e(b),b)) Thm*   Thm*  (A:Type, f:(AAB). (a:A. R((Diag f wrt x. e(x))(a),f(a,a))))	[diagonalization]
Thm*  B:Type, e:(BB), A:Type, f:(AAB). (Diag f wrt y. e(y))  AB	[diagonalize_wf]
Thm*  f:(AB). f  A{y:B| x:A. f(x) = y }	[range_restriction_indep]
Thm*  B:(AType), f:(x:AB(x)). f  x:A{f(x):B(x)}	[range_restriction_dep]
Thm*  A,B:Type, P:(ABProp). Thm*  (x:A. !y:B. P(x,y))  (!f:(AB). x:A. P(x,f(x)))	[unique_indep_fun_description]
Thm*  (x:A. !y:B. P(x,y))  (f:(AB). x:A. P(x,f(x)))	[indep_fun_description]
Thm*  (x:A. y:B. Q(x,y))  (f:(AB). x:A. Q(x,f(x)))	[ax_choice_version3]
Thm*  (x:A. y:B. Q(x,y))  (f:(AB). x:A. Q(x,f(x)))	[ax_choice_version2]
Thm*  B:(AType), P:(x:AB(x)Prop). Thm*  (x:A. !y:B(x). P(x,y))  (!{f:(x:AB(x))| x:A. P(x,f(x)) })	[unique_fun_description2]
Thm*  B:(AType), P:(x:AB(x)Prop). Thm*  (x:A. !y:B(x). P(x,y))  (!f:(x:AB(x)). x:A. P(x,f(x)))	[unique_fun_description]
Thm*  (x:A. !y:B(x). P(x,y))  (f:(x:AB(x)). x:A. P(x,f(x)))	[fun_description]
Thm*  (x:A. y:B(x). Q(x,y))  (f:(x:AB(x)). x:A. Q(x,f(x)))	[dep_ax_choice_version2]
Thm*  f,g:(AB). f = g  (x:A. f(x) = g(x))	[indep_fun_extensional]
Thm*  (!A)  (!x:A. True)	[inhabited_uniquely_vs_exists_unique]
Thm*  P:(AType). (x:A. Dec(P(x)))  (!{p:(A)| x:A. p(x)  P(x) })	[dec_pred_imp_bool_decider_exists]
Thm*  (x:T. Dec(E(x)))  (f:(T). x:T. f(x)  E(x))	[dec_pred_iff_some_boolfun]
Thm*  P:(AProp). (!u:A. P(u))  (y,z:A. P(y)  P(z)  y = z)	[exists_unique_elim]
Thm*  R:(AAProp).  Thm*  (EquivRel x,y:A. R(x,y)) Thm*   Thm*  (x:A. R(x,x) & (y:A. R(x,y)  R(y,x) & (z:A. R(y,z)  R(x,z))))	[equivrel_characterization]
Thm*  (Set:Type, :(SetSetProp). Thm*  (P:(SetProp). p:Set. x:Set. (x  p)  P(x))	[RussellsParadox_Frege2]
Thm*  (A:Type, Q:(AAProp). P:(AProp). p:A. x:A. Q(x,p)  P(x))	[RussellsParadox_Frege]
Thm*  (P  P)	[no_prop_iff_its_neg]
Thm*  (A Discrete)  (e:(AA). IsEqFun(A;e))	[discrete_vs_bool2]
Thm*  (A Discrete)  (e:(AA). x,y:A. (x e y)  x = y)	[discrete_vs_bool]
Thm*  A:Type. (A Discrete)  Prop	[is_discrete_wf]
Thm*  {x:A| if b P(x) else Q(x) fi } Thm*  =ext Thm*  if b {x:A| P(x) } else {x:A| Q(x) } fi	[ifthenelse_distr_subtype]
Thm*  {x:A| P(x) } =ext {x:A| P(x) }	[subset_squash_exteq]
Thm*  (x:A. B(x)  B'(x))  ({x:A| B(x) } =ext {x:A| B'(x) })	[subset_sq_exteq]
Thm*  (x:A. B(x)  B'(x))  {x:A| B(x) }  {x:A| B'(x) }	[set_inc_wrt_imp_sq]
Thm*  x:A. B(x)  x  {x:A| B(x) }	[squash_to_subset]
Thm*  x:{x:A| B(x) }. B(x)	[subset_to_squash]
Thm*  (x:A. B(x)  B'(x))  ({x:A| B(x) } =ext {x:A| B'(x) })	[subset_exteq]
Thm*  {x:{x:A| P(x) }| Q(x) } =ext {x:A| P(x) & Q(x) }	[exteq_subset_vs_and]
Thm*  P XOR Q  (Q  P) & Dec(P)	[xor_vs_neg_n_dec]
Thm*  P,Q:Prop. (P XOR Q)  Prop	[xor_wf]
Thm*  (x:A. B(x)  B'(x))  {x:A| B(x) }  {x:A| B'(x) }	[set_inc_wrt_imp]
Thm*  P  P	[sq_sq_iff_sq]
Thm*  Dec(P)  Dec(P)	[dec_imp_dec_sq]
Thm*  (P)  P	[sq_not_iff_sq]
Thm*  P  P	[not_sq_iff_sq]
Thm*  (A)  (!(AB))	[unique_fn_over_empty]
Thm*  (!A)  (x:A. y:A. x = y)	[inhabited_uniquely_elim]
Thm*  (!A)  (x:A. y:A. x = y)	[inhabited_uniquely_vs_exists]
Thm*  (A)  (x:A. True)	[inhabited_vs_exists]
Thm*  F:(PropProp). (P:Prop. F(P))  (A:Type. F(A))	[inhab_rep_eqv]
Thm*  A:Type. P = (A)  Prop	[inhab_rep_axiom]
Thm*  (x:A. B(x))  ((x:AB(x)))	[inhab_choice]
Thm*  {a:{a:A}} =ext {a:A}	[singleton_singleton_self]
Thm*  x:{a:A}. x = a  {a:A}	[singleton_eq_in_self]
Thm*  B:(AType), P:(AProp). Thm*  (i:{i:A| P(i) }B(i)) =ext {v:(i:AB(i))| P(v/x,y. x) }	[exteq_sigma_st_dom]
Thm*  (x:T. Q(x))  (x:T. Q(x))	[not_over_exists_imp]
Thm*  A,B:Type. AB  Type	[isect_two_wf]
Thm*  Dec(P)  (b:. b  P)	[decbl_iff_some_bool]
Thm*  B:Prop(given A). (A & B)  Prop	[cand_is_prop]
Thm*  Q:Prop(given P). Dec(P)  (P  Dec(Q))  Dec(P & Q)	[decidable__cand]
Thm*  Q:Prop(given P). P  Q  Prop	[guarded_prop_to_prop]
Thm*  Q  Q  Q	[or_fused]
Thm*  P  Q  P  Q	[disjunct_elim]
Thm*  (P:Prop. P  P)  (P:Prop. P  P)	[negnegelim_vs_bivalence]
Def  x is the u:A. P(u) == P(x) & (u:A. P(u)  u = x)	[is_the]
Def  A Discrete == x,y:A. Dec(x = y)	[is_discrete]
Def  !A == {x:A| y:A. x = y }	[inhabited_uniquely]
Def  A =ext B == (x:A. x  B) & (x:B. x  A)	[exteq]
Def   x:A st P(x). Q(x) == x:A. P(x)  Q(x)	[allst]

In prior sections: core well fnd int 1 bool 1 rel 1 quot 1

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