Nuprl - Proof: nsub inj lop typing 1 1

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

1. a :

2. b :

3. f :

b
4. Inj(

b; f)

(a-1) inj

{x:

x = f(a-1) }

By:	Analyze THEN FunExtensionality

Generated subgoals:

1 5. x : (a-1)
f(x) {x:b| x = f(a-1) }
3 steps

2 Inj((a-1); {x:b| x = f(a-1) }; f)
5 steps

About:

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

1	5. x : (a-1) f(x) {x:b\| x = f(a-1) }	3 steps
2	Inj((a-1); {x:b\| x = f(a-1) }; f)	5 steps