Nuprl - Proof: nsub inj lop typing 1 1 2 1

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

1. a :

2. b :

3. f :

b
4. Inj(

b; f)
5. a1 :

(a-1)
6. a2 :

(a-1)
7. f(a1) = f(a2)

a1 = a2

By:	FwdThru: Hyp:4 on [ Hyp:-1 ]

Generated subgoals:

None

About:

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