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* (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* 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* Stable{P}	[stable__not]
Thm* Dec(A)  (A  B)  Dec(B)	[iff_preserves_decidability]
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]
Def XM == P:Prop. Dec(P)	[xmiddle]

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