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

is mentioned by

Thm* a:T, Q:(TProp). (a = !x:T. Q(x))  a  {!x:T | Q(x)}	[uni_sat_imp_in_uni_set]
Thm* a:T, x:{a:T}. x = a  T	[singleton_properties]
Thm* B:(AType), p:(x:AB(x)), C:Type, b:(x:AB(x)C). Thm* (p/x,y. b(x,y)) = b(1of(p),2of(p))	[spread_to_pi12]
Thm* B:(AType), p:(x:AB(x)), C,D:Type, f:(CD), b:(x:AB(x)C). Thm* f(p/x,y. b(x,y)) = (p/x,y. f(b(x,y)))	[fun_thru_spread]
Thm* A,B:Type, a:A, b:(AB). let x = a in b(x)  B	[let_wf]
Thm* (P  Q)  (Q  P)  (P  Q)	[implies_antisymmetry]
Thm* (P  Q)  (P  Q)	[squash_functionality_wrt_iff]
Thm* (P  Q)  P  Q	[squash_functionality_wrt_implies]
Thm* (P1  P2)  (Q1  Q2)  P1  Q1  P2  Q2	[or_functionality_wrt_implies]
Thm* (P1  P2)  (Q1  Q2)  (P1  Q1  P2  Q2)	[or_functionality_wrt_iff]
Thm* (P  Q)  P  Q	[not_functionality_wrt_implies]
Thm* (P  Q)  (P  Q)	[not_functionality_wrt_iff]
Thm* P,Q:(SProp). Thm* S = T  (x:S. P(x)  Q(x))  (x:S. P(x))  (y:T. Q(y))	[exists_functionality_wrt_implies]
Thm* P,Q:(SProp). Thm* S = T  (x:S. P(x)  Q(x))  ((x:S. P(x))  (y:T. Q(y)))	[exists_functionality_wrt_iff]
Thm* P,Q:(SProp). Thm* S = T  (z:S. P(z)  Q(z))  (x:S. P(x))  (y:T. Q(y))	[all_functionality_wrt_implies]
Thm* P,Q:(SProp). Thm* S = T  (x:S. P(x)  Q(x))  ((x:S. P(x))  (y:T. Q(y)))	[all_functionality_wrt_iff]
Thm* (P1  P2)  (Q1  Q2)  ((P1  Q1)  (P2  Q2))	[iff_functionality_wrt_iff]
Thm* (P  Q)  (Dec(P)  Dec(Q))	[decidable_functionality]
Thm* (P1  P2)  (Q1  Q2)  (P1  Q1)  P2  Q2	[implies_functionality_wrt_implies]
Thm* (P1  P2)  (Q1  Q2)  ((P1  Q1)  (P2  Q2))	[implies_functionality_wrt_iff]
Thm* (P1  P2)  (Q1  Q2)  P1 & Q1  P2 & Q2	[and_functionality_wrt_implies]
Thm* (P1  P2)  (Q1  Q2)  (P1 & Q1  P2 & Q2)	[and_functionality_wrt_iff]
Thm* (P  Q)  (Q  R)  P  R	[implies_transitivity]
Thm* (P  Q)  (Q  R)  (P  R)	[iff_transitivity]
Thm* Q:(TProp). (x:T. Q(x))  (x:T. Q(x))	[not_over_exists]
Thm* B:(TProp). (x:T. A & B(x))  A & (x:T. B(x))	[exists_over_and_r]
Thm* A  True  True	[or_true_r]
Thm* True  A  True	[or_true_l]
Thm* A  False  A	[or_false_r]
Thm* False  A  A	[or_false_l]
Thm* A & True  A	[and_true_r]
Thm* True & A  A	[and_true_l]
Thm* A & False  False	[and_false_r]
Thm* False & A  False	[and_false_l]
Thm* Dec(A)  ((A & B)  A  B)	[not_over_and]
Thm* A  B  (A & B)	[not_over_and_b]
Thm* (A  B)  A & B	[not_over_or_a]
Thm* (A  B)  A & B	[not_over_or]
Thm* A  B  B  A	[or_comm]
Thm* A  (B  C)  (A  B)  C	[or_assoc]
Thm* A & B  B & A	[and_comm]
Thm* A & (B & C)  (A & B) & C	[and_assoc]
Thm* (A  B)  (B  A)	[iff_symmetry]
Thm* Dec(A)  (A  A)	[dneg_elim_a]
Thm* Dec(A)  A  A	[dneg_elim]
Thm* SqStable(P)  (P  P)	[squash_elim]
Thm* Dec(P)  SqStable(P)	[sq_stable_from_decidable]
Thm* SqStable(P)	[sq_stable__not]
Thm* Stable{P}  SqStable(P)	[sq_stable__from_stable]
Thm* SqStable(P)	[sq_stable__squash]
Thm* x,y:A. SqStable(x = y)	[sq_stable__equal]
Thm* P:(AProp). (x:A. SqStable(P(x)))  SqStable(x:A. P(x))	[sq_stable__all]
Thm* SqStable(P)  SqStable(Q)  SqStable(P  Q)	[sq_stable__iff]
Thm* SqStable(Q)  SqStable(P  Q)	[sq_stable__implies]
Thm* SqStable(P)  SqStable(Q)  SqStable(P & Q)	[sq_stable__and]
Thm* Dec(P)  Stable{P}	[stable__from_decidable]
Thm* f,g:(AB). (x:A. Stable{f(x) = g(x)})  Stable{f = g}	[stable__function_equal]
Thm* Stable{P}	[stable__not]
Thm* Dec(A)  (A  B)  Dec(B)	[iff_preserves_decidability]
Thm* a,b:Atom. Dec(a = b)	[decidable__atom_equal]
Thm* i,j:. Dec(i = j)	[decidable__int_equal]
Thm* Dec(P)  Dec(Q)  Dec(P  Q)	[decidable__iff]
Thm* Dec(P)  Dec(Q)  Dec(P  Q)	[decidable__implies]
Thm* Dec(P)  Dec(Q)  Dec(P & Q)	[decidable__and]
Thm* Dec(P)  Dec(Q)  Dec(P  Q)	[decidable__or]
Thm* a:Unit. a =	[unit_triviality]
Thm* B:(AType), p:(a:AB(a)). <1of(p),2of(p)> = p  a:AB(a)	[pair_eta_rw]
Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p)  B(1of(p))	[pi2_wf]
Thm* A:Type, a:A. (a  A)  Type	[member_wf]
Def a = !x:T. Q(x) == Q(a) & (a':T. Q(a')  a' = a)	[uni_sat]
Def {!x:T | P(x)} == {x:T| P(x) & (y:T. P(y)  y = x) }	[unique_set]
Def XM == P:Prop. Dec(P)	[xmiddle]
Def S  T == x:S. x  T	[subtype]

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