Nuprl - Proof: hnil def 1 2 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hnil def 1 2 1 1 1

1. 'a : S
2. n :

if n<

0 then nil[n] else arb('a) fi = (@

e:'a. true

)

By:	BifCase THEN Simp THEN StrongAuto

Generated subgoal:

1 3. n<0
arb('a) = (@e:'a. true)
1 step

About:

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