Nuprl - Proof: nsub inj fill typing 1 1 1 1

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

1. a :

2. b :

3. j :

b
4. f :

(a-1)

{x:

x = j }
5. Inj(

(a-1); {x:

x = j }; f)
6. i :

if i=

a-1

j else f(i) fi

By:	SplitITE Concl

Generated subgoals:

None

About:

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