Nuprl - Proof: hprim rec wd

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hprim rec wd

'a:S.

all

(

x:'a. all

(

x:'a. (

f:'a

hnum

'a. all

(

x:'a. (

f:'a

hnum

'a. (

m:hnum. equal

(

x:'a. (

f:'a

hnum

'a. (

m:hnum. (prim_rec(x,f,m)

(

x:'a. (

f:'a

hnum

'a. (

m:hnum. ,prim_rec_fun(x,f,m,pre(m))))))

By:	Unab [`hprim_rec`] THEN HN THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

None

About:

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