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

is mentioned by

Thm* x:. y:. yyx & x<(y+1)(y+1)	[sfa_doc_nat_sqrt]
Thm* x,y:. x<y & (z:. z<x  y<z)	[sfa_doc_simple_existential_2]
Thm* x:. xx = 4	[sfa_doc_simple_existential_1]
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* f,g:(). Thm* (x:. f zero beyond x) & (x:. g zero beyond x) Thm*  Thm* (x:. (i.if i even f(i) else g(i) fi) zero beyond x)	[sfa_doc_alternate_zero_beyond]
Thm* P  Q  (x:. (x = 0  P) & (x  0  Q))	[sfa_doc_or_dec]
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* B:(AProp). (x:A. B(x))  (C:Prop. (x:A. B(x)  C)  C)	[sfa_doc_some_via_so]
Thm* s:Sexpr(A). (x:A. s = Inj(x))  (s1,s2:Sexpr(A). s = Cons(s1;s2))	[sfa_doc_sexpr_case_thm]
Thm* f:{f:()| x:. f(x) }, i:. i<mu(f)  f(i)	[kleene_minimize_is_lb]
Thm* f:{f:()| x:. f(x) }. f(mu(f))	[kleene_minimize_is_fp]
Thm* mu  {f:()| x:. f(x) }	[kleene_minimize_wf]
Thm* f:{f:()| x:. f(x) }. f(0)  (x.f(1+x))  {f:()| x:. f(x) }	[kleene_tail]
Def  mod k == x,y://(m:. x-y = mk)	[sfa_doc_sample_intmod]

In prior sections: core fun 1 int 2

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html