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

is mentioned by

Thm* m,n:. n<m  (x:. x+n = m  )	[less_add]
Thm* m:. pre(m) = nnsub(m;1)	[pre_sub1]
Thm* m:. nnsub(m+1;1) = m	[suc_sub1]
Thm* m,n:. m+1<n+1  m<n	[less_mono_eq]
Thm* m,n:. m+1<n+1  m<n	[less_mono_rev]
Thm* m:. m = 0    (n:. m = n+1  )	[num_cases]
Thm* m,n:. m+n = n+m	[add_sym]
Thm* n,m:. Thm* 0+m = m   & m+0 = m   & m+1+n = m+n+1   & m+(n+1) = (m+n)+1	[add_clauses]
Thm* m,n:. (m+n)+1 = m+(n+1)	[add_suc]
Thm* m:. m+0 = m	[add_0]
Thm* n:. 0 = n+1	[suc_not]

In prior sections: core

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