??(m+1); (k+1); f) 
Bij(m; k; Replace value k by f(m) in f)
| 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.
(m+1); (k+1); f) (Replace value k by f(m) in f) 
m
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 })
(m+1); (k+1); f)
Thm*
Thm* (i:m. f(i) = k (Replace value k by f(m) in f)(i) = f(m) k)| 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 })
(m+1); (k+1); f)
Thm*
Thm* (i:m. f(i) = k (Replace value k by f(m) in f)(i) = f(i) k)| 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 })
(m+1); (k+1); f) Inj(m; k; Replace value k by f(m) in f)| 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:
 |  |  |  |  |  |
 |  |  |  |  |  |