'a:S.
all
(
n:hnum. all
(n:hnum. (f:'a 
'a. all
(n:hnum. (f:'a 'a. (x:'a. equal
(n:hnum. (f:'a 'a. (x:'a. (exists
(n:hnum. (f:'a 'a. (x:'a. ((fun:hnum 'a. simp_rec_rel(fun,x,f,n))
(n:hnum. (f:'a 'a. (x:'a. ,and
(n:hnum. (f:'a 'a. (x:'a. ,(equal(simp_rec_fun(x,f,n,0),x)
(n:hnum. (f:'a 'a. (x:'a. ,,all
(n:hnum. (f:'a 'a. (x:'a. ,,(m:hnum. implies
(n:hnum. (f:'a 'a. (x:'a. ,,(m:hnum. (lt(m,n)
(n:hnum. (f:'a 'a. (x:'a. ,,(m:hnum. ,equal
(n:hnum. (f:'a 'a. (x:'a. ,,(m:hnum. ,(simp_rec_fun(x,f,n,suc(m))
(n:hnum. (f:'a 'a. (x:'a. ,,(m:hnum. ,,f
(n:hnum. (f:'a 'a. (x:'a. ,,(m:hnum. ,,(simp_rec_fun(x,f,n,m))))))))))
