Nuprl - Proof: nsub inj factorial2 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub inj factorial2 2

1. b :

2. 0<b
3. (

(b-1) inj

(b-1)) ~

((b-1)!)

(

b inj

b) ~

(b!)

By:	Rewrite by Thm* a,b:. (a inj b) ~ (b((a-1) inj (b-1)))

Generated subgoal:

1 (b((b-1) inj (b-1))) ~ (b!)
3 steps

About:

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