Nuprl - Proof: nsub inj factorial tail 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub inj factorial tail 1 1

1. a :

a1:

. a1<a

(

. (

a1 inj

b) ~

(b!a1))
3. b :

4. a

(

a inj

b) ~

(b!a)

By:	Decide: a = 0

Generated subgoals:

1 5. a = 0
(a inj b) ~ (b!a)
5 steps

2 5. a = 0
(a inj b) ~ (b!a)
5 steps

About:

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

1	5. a = 0 (a inj b) ~ (b!a)	5 steps
2	5. a = 0 (a inj b) ~ (b!a)	5 steps