is mentioned by

Thm* A:Type, a:A, xs:A List. (a list xs)  Prop	[sfa_doc_inlist_wf]
Thm* x: List, y:. y greater-bounds x  Prop	[sfa_doc_greater_list_bound_wf]
Thm* P:(AProp). (x:A. Dec(P(x)))  (f:(A). x:A. P(x)  f(x))	[sfa_doc_bool_vs_decidable_fun]
Thm* Dec(P)  (b:. P  b)	[sfa_doc_bool_vs_decidable]
Thm* x:, f:(). f zero beyond x  Prop	[sfa_doc_props_as_types_example1_wf]
Thm* P  Q  (x:. (x = 0  P) & (x  0  Q))	[sfa_doc_or_dec]
Thm* f:().  Thm* (n:. f(n) = 0) Thm*  Thm* (n:. if f(n)=0 False else C:Prop{1}. C fi)  Prop{1}	[sfa_doc_predicativity_sample8]
Thm* R:(A(A List)PropProp).  Thm* P:((A List)Prop).  Thm* (P(nil)  Q) & (a:A, x:A List. P(a.x)  R(a,x,P(x)))	[sfa_doc_listind_via_so]
Thm* a,b:A. a = b  (P:(AProp). P(a)  P(b))	[sfa_doc_equal_via_so]
Thm* B:(AProp). (x:A. B(x))  (C:Prop. (x:A. B(x)  C)  C)	[sfa_doc_some_via_so]
Thm* False  (C:Prop. C)	[sfa_doc_false_via_so]
Thm* (A  B)  (C:Prop. ((A  B)  (B  A)  C)  C)	[sfa_doc_iff_via_so]
Thm* A  (C:Prop. A  C)	[sfa_doc_not_via_so]
Thm* A  B  (C:Prop. (A  C)  (B  C)  C)	[sfa_doc_or_via_so]
Thm* A & B  (C:Prop. (A  B  C)  C)	[sfa_doc_and_via_so]
Thm* A:Prop, B:Type(given A). B(given A)  Type	[sfa_doc_guarded_typing]
Thm* A:Prop, B:Prop(given A). (A  B)  Prop	[sfa_doc_imp_typing]
Thm* A:Type, P:(AProp), n:, X:(A^n). ( u in X: A^n. P(u))  Prop	[sfa_doc_ntuple_contains_wf]
Thm* A:Prop, B:Prop(given A). (A & B)  Prop	[sfa_doc_and_typing]
Thm* P:(AProp), B:(x:AType(given P(x))). Thm* x:{u:A| P(u) }B(x) =ext x:AB(x)(given P(x))	[sfa_doc_exteq_gfun2]
Thm* B:(AProp), C:({u:A| B(u) }Type). Thm* x:{u:A| B(u) }C(x) =ext x:AC(x)(given B(x))	[sfa_doc_exteq_gfun]
Thm* P:(AProp). {x:A| P(x) }Prop =ext x:AProp(given P(x))	[sfa_doc_exteq_gprop]
Def HigherConsequence{i}(P) == {X:Prop{i'}| P  X }	[sfa_doc_le_parm_sample_def]

In prior sections: core well fnd int 1 bool 1 rel 1 fun 1 int 2 list 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html