IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(Replace value k by f(m) in f) is intended to take a bijection between two collections of integers making a new one in which k is deleted from the range and m is deleted from the domain. Here is a theorem to this effect as well as one specialized for our standard finite types ?.

Thm*  Bij((m+1); (k+1); f Bij(mk; Replace value k by f(m) in f)

Thm*  Bij({u:P(u) }; {v:Q(v) }; f)
Thm*
Thm*  (m:{u:P(u) }, k:{v:Q(v) }.
Thm*  (Bij({u:P(u) & u = m }; {v:Q(v) & v = k };
Thm*  (Bij(Replace value k by f(m) in f))

Although the special theorem follows from the more general one, they have been given independent proofs, as is the case for various lemmas supporting them.
We provide independent proofs of the special cases because they're a bit easier to read (Auto can do more on its own), and may serve as a guides to the more general ones.

Thm*  Inj((m+1); (k+1); f (Replace value k by f(m) in f mk
Thm*  Inj({k:P(k) }; {k:Q(k) }; f)
Thm*
Thm*  (m:{u:P(u) }, k:{v:Q(v) }.
Thm*  ((Replace value k by f(m) in f)
Thm*  ( {u:P(u) & u = m }{v:Q(v) & v = k })

Thm*  Inj((m+1); (k+1); f)
Thm*
Thm*  (i:mf(i) = k  (Replace value k by f(m) in f)(i) = f(mk)

Thm*  Inj({u:P(u) }; {u:Q(u) }; f)
Thm*
Thm*  (m:{u:P(u) }, k:{v:Q(v) }, i:{u:P(u) & u = m }.
Thm*  (f(i) = k
Thm*  (
Thm*  ((Replace value k by f(m) in f)(i) = f(m {v:Q(v) & v = k })

Thm*  Inj((m+1); (k+1); f)
Thm*
Thm*  (i:mf(i) = k  (Replace value k by f(m) in f)(i) = f(ik)

Thm*  Inj({u:P(u) }; {u:Q(u) }; f)
Thm*
Thm*  (m:{u:P(u) }, k:{v:Q(v) }, i:{u:P(u) & u = m }.
Thm*  (f(i) = k
Thm*  (
Thm*  ((Replace value k by f(m) in f)(i) = f(i {v:Q(v) & v = k })

Thm*  Inj((m+1); (k+1); f Inj(mk; Replace value k by f(m) in f)
Thm*  Inj({u:P(u) }; {v:Q(v) }; f)
Thm*
Thm*  (m:{u:P(u) }, k:{v:Q(v) }.
Thm*  (Inj({u:P(u) & u = m }; {v:Q(v) & v = k };
Thm*  (Inj(Replace value k by f(m) in f))

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