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

is mentioned by

Thm* n:. odd(n)  (m:. n = 2m+1  )	[odd_exists]
Thm* n:. even(n)  (m:. n = 2m  )	[even_exists]
Thm* n:. (even(n)  (m:. n = 2m  )) & (odd(n)  (m:. n = 2m+1  ))	[even_odd_exists]
Thm* m,n:. mn  (x:. n = m+x  )	[less_eq_exists]
Thm* m,n:. mn  (x:. n = m+x  )	[less_equal_add]
Thm* n:. m:. n = (0+1+1)m    n = (0+1+1)m+1	[odd_or_even]

In prior sections: core fun 1 hol hol bool hol prim rec int 2 hol arithmetic 3 hol arithmetic 4

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