Nuprl - Proof: nsub inj lop typing 1

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

1. a :

2. b :

3. f :

a inj

(a-1) inj

{x:

x = f(a-1) }

By:

Analyze-1

Generated subgoal:

1 3. f : ab
4. Inj(a; b; f)
f (a-1) inj {x:b| x = f(a-1) }
9 steps

About:

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