Nuprl - DiscreteMath LEMMAs for delete_fenum_value_is_inj

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

Theorem	Name
Thm* Inj({u:\| P(u) }; {v:\| Q(v) }; 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({u:\| P(u) & u = m }; {v:\| Q(v) & v = k }; Thm* (& Inj(Replace value k by f(m) in f))	[delete_fenum_value_is_inj_genW]
cites the following:
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 })	[delete_fenum_value_comp1_gen]
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 })	[delete_fenum_value_comp2_gen]

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