Nuprl - Proof: hsimp rec exists

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

'a:S.

all

(

x:'a. all

(

x:'a. (

f:'a

'a. all

(

x:'a. (

f:'a

'a. (

n:hnum. exists

(

x:'a. (

f:'a

'a. (

n:hnum. (

fun:hnum

'a. simp_rec_rel(fun,x,f,n)))))

By:	HOL "hsimp_rec_exists"

Generated subgoals:

None

About:

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