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

is mentioned by

Thm* A:Type. Sexpr(A) =ext (Sexpr(A)Sexpr(A))+A	[sfa_doc_sexpr_fp]
Thm* f,g:(AB). f = g  (x:A. f(x) = g(x))	[sfa_doc_fun_ext]
Thm* z:A+B. z = InjCase(z; u. inl(u); v. inr(v))	[sfa_doc_reinject]
Thm* as:T List. (i.as[i]){||as||} = as	[sfa_doc_listify_select_id]
Thm* B:(AType), p:(u:AB(u)). p = <p.1,p.2>  a:AB(a)	[sfa_doc_pairing_projs]
Thm* f:(C,D:Type. CDDC), A,B:Type, a:A, b:B. f(<a,b>) = <b,a>  BA	[sfa_doc_type_poly_swap]
Thm* T:Type, f:(D:Type. DT). f(f)  T	[sfa_doc_type_poly_ap_doppelganger]
Thm* A  Top	[sfa_doc_top_is_top]
Thm* (x.whatever) = (x.x)  VoidA	[sfa_doc_whatever_in_void_dom_fun]
Thm* VoidA =ext {x.x:VoidA}	[sfa_doc_void_dom_fun_degenerate]
Thm* Void  A	[sfa_doc_void_is_bottom]
Thm* VoidA =ext Void	[sfa_doc_void_cross_is_void]
Thm* f:(( mod 2)A). f  A	[sfa_doc_polymorph_example1]
Thm* k:.   ( mod k)	[sfa_doc_int_sub_int_mod]
Thm* f:(D:Type. DT), A:Type, a:A, B:Type, b:B. f(a) = f(b)  T	[sfa_doc_type_poly_constant]
Thm* f:(D:Type. DD), A:Type, a:A. f(a) = a	[sfa_doc_type_poly_identity]
Thm* f:(D:Type. D(D List)), A:Type, a:A, B:Type, b:B. Thm* ||f(a)|| = ||f(b)||	[sfa_doc_type_poly_len_const]
Thm* f:(D:Type. D(D List)), A:Type, a,x:A. x list f(a)  x = a	[sfa_doc_type_poly_mem_const]
Thm* a:A, w:{a:A} List. z:A. z list w  z = a	[sfa_doc_inlist_singleton_const]
Thm* A:Type, a:A, xs:A List. (a list xs)  Prop	[sfa_doc_inlist_wf]
Thm* x:. y:. yyx & x<(y+1)(y+1)	[sfa_doc_nat_sqrt]
Thm* A:Type, a:A, e:(AA), i:. i steps of e from a  A	[sfa_doc_sequence_rel_wf]
Thm* x: List, y:. y greater-bounds x  Prop	[sfa_doc_greater_list_bound_wf]
Thm* r,s:T, x:(r = s  T). x = *  (r = s  T)	[sfa_doc_eq_mem_unique]
Thm* B:(AType), a:A. (x:A. B(x))  B(a)	[sfa_doc_isect_subtype]
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* a,b:. max(a;b)	[sfa_doc_max_int_wf]
Thm* i:. i even	[sfa_doc_even_wf]
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,b,c:X. Thm* Reverse(Cons(Inj(a);Cons(Inj(b);Inj(c)))) Thm* = Thm* Cons(Cons(Inj(c);Inj(b));Inj(a))	[sfa_doc_sexpr_reverse_example]
Thm* A:Type, e:Sexpr(A). Reverse(e)  Sexpr(A)	[sfa_doc_sexpr_reverse_wf]
Thm* A:Type, s:Sexpr(A). Size(s) = 1    sexprAtom(s)  A	[sfa_doc_sexpr_atom_wf]
Thm* s:Sexpr(A). Size(s)  1    Size(sexprCdr(s))<Size(s)	[sfa_doc_sexprcdrsize]
Thm* s:Sexpr(A). Size(s)  1    Size(sexprCar(s))<Size(s)	[sfa_doc_sexprcarsize]
Thm* A:Type, s:Sexpr(A). Size(s)	[sfa_doc_sexpr_size_wf]
Thm* A:Type, s:Sexpr(A). sexprCdr(s)  Sexpr(A)	[sfa_doc_sexpr_cdr_wf]
Thm* A:Type, s:Sexpr(A). sexprCar(s)  Sexpr(A)	[sfa_doc_sexpr_car_wf]
Thm* A:Type, C:(Sexpr(A)Type), s:Sexpr(A), Thm* f:(s1,s2:Sexpr(A)C(Cons(s1;s2))), g:(x:AC(Inj(x))). Thm* (Case of s :  Inj(x)  g(x) ; Cons(s1;s2)  f(s1,s2))  C(s)	[sfa_doc_sexpr_cases_wf]
Thm* s:Sexpr(A). (x:A. s = Inj(x))  (s1,s2:Sexpr(A). s = Cons(s1;s2))	[sfa_doc_sexpr_case_thm]
Thm* A:Type, a:A. Inj(a)  Sexpr(A)	[sfa_doc_sexpr_inj_wf]
Thm* A:Type, s1,s2:Sexpr(A). Cons(s1;s2)  Sexpr(A)	[sfa_doc_sexpr_cons_wf]
Thm* A:Type. Sexpr(A)  Type	[sfa_doc_sexpr_wf]
Thm* A:Type, P:(AProp), n:, X:(A^n). ( u in X: A^n. P(u))  Prop	[sfa_doc_ntuple_contains_wf]
Thm* n:. n2  (A^n) = A(A^(n-1))	[sfa_doc_ntuple_is_prod]
Thm* A:Type, n:. (A^n)  Type	[sfa_doc_ntuple_wf]
Thm* x:{x:| (x rem 2) = 0 }. x!	[sfa_doc_factorial2_wf]
Thm* x:. x!	[sfa_doc_factorial_wf]
Thm* a:(0  ). a = *	[sfa_doc_memtype_is_singleton]
Thm* k:.  mod k  Type	[sfa_doc_sample_intmod_wf]
Thm* A:Prop, B:Prop(given A). (A & B)  Prop	[sfa_doc_and_typing]
Thm* k:. 0<k & (2  k)<1  2<k	[sfa_doc_cand_example]
Thm* A:Type, B:Type(given A). AB  Type	[sfa_doc_indep_fun_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]
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* f:{f:()| x:. f(x) }. f(0)  (x.f(1+x))  {f:()| x:. f(x) }	[kleene_tail]
Def y greater-bounds x == i:||x||. x[i]<y	[sfa_doc_greater_list_bound]
Def f zero beyond x == y:. x<y  f(y) = 0	[sfa_doc_props_as_types_example1]
Def Induction for x:. P(x) == P(0) & (x:. P(x)  P(x+1))  (x:. P(x))	[sfa_doc_indscheme]
Def A =ext B == (X:A. X  B) & (X:B. X  A)	[sfa_doc_exteq]

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

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