Nuprl - Proof: nsub inj fill typing

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

, b:

, j:

b, f:(

(a-1) inj

{x:

x = j }).

(

i.if i=

a-1

j else f(i) fi)

a inj

By:

Auto

Generated subgoal:

1 1. a :
2. b :
3. j : b
4. f : (a-1) inj {x:b| x = j }
(i.if i=a-1 j else f(i) fi) a inj b
12 steps

About:

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