Nuprl - Proof: nsub inj factorial

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A more direct proof of this fact is in nsub inj factorial2.

. (

k inj

k) ~

(k!)

By:	Def of k! THEN BackThru: Thm* (a inj b) ~ (b!a)

Generated subgoals:

None

About:

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