Nuprl - DiscreteMath LEMMAs for delete_fenum_value_is_inj

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

Rank	Theorem	Name
2	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))	[delete_fenum_value_is_inj_gen]
cites the following:
1	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]

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