Nuprl - Proof: nsub inj fill typing 1

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

1. a :

2. b :

3. j :

b
4. f :

(a-1) inj

{x:

x = j }

(

i.if i=

a-1

j else f(i) fi)

a inj

By:

Analyze-1

Generated subgoal:

1 4. f : (a-1){x:b| x = j }
5. Inj((a-1); {x:b| x = j }; f)
(i.if i=a-1 j else f(i) fi) a inj b
11 steps

About:

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