'a:S, n:
, f:('a
'a), x:'a.
Thm* (
fun:('a). simp_rec_rel(fun,x,f,n))
Thm*
Thm* simp_rec_fun(x,f,n,0) = x
Thm* & (
m:. m<n 
simp_rec_fun(x,f,n,m+1) = f(simp_rec_fun(x,f,n,m)))'a:S.
Thm* all
Thm* (
n:hnum. all
Thm* (
n:hnum. (f:'a
Thm* (
n:hnum. ( 'a. all
Thm* (
n:hnum. ( 'a. (x:'a. equal
Thm* (
n:hnum. ( 'a. (x:'a. (exists(fun:hnum 'a. simp_rec_rel(fun,x,f,n))
Thm* (
n:hnum. ( 'a. (x:'a. ,and
Thm* (
n:hnum. ( 'a. (x:'a. ,(equal(simp_rec_fun(x,f,n,0),x)
Thm* (
n:hnum. ( 'a. (x:'a. ,,all
Thm* (
n:hnum. ( 'a. (x:'a. ,,(m:hnum. implies
Thm* (
n:hnum. ( 'a. (x:'a. ,,(m:hnum. (lt(m,n)
Thm* (
n:hnum. ( 'a. (x:'a. ,,(m:hnum. ,equal
Thm* (
n:hnum. ( 'a. (x:'a. ,,(m:hnum. ,(simp_rec_fun(x,f,n,suc(m))
Thm* (
n:hnum. ( 'a. (x:'a. ,,(m:hnum. ,,f(simp_rec_fun(x,f,n,m))))))))))