'a:S.
all
(
r:hprod((hnum 
'a); hnum
(r:hprod(). equal
(r:hprod(). (is_list_rep(r)
(r:hprod(). ,exists
(r:hprod(). ,(f:hnum 'a. exists
(r:hprod(). ,(f:hnum 'a. (n:hnum. equal
(r:hprod(). ,(f:hnum 'a. (n:hnum. (r
(r:hprod(). ,(f:hnum 'a. (n:hnum. ,pair
(r:hprod(). ,(f:hnum 'a. (n:hnum. ,((m:hnum. cond
(r:hprod(). ,(f:hnum 'a. (n:hnum. ,((m:hnum. (lt(m,n)
(r:hprod(). ,(f:hnum 'a. (n:hnum. ,((m:hnum. ,f(m)
(r:hprod(). ,(f:hnum 'a. (n:hnum. ,((m:hnum. ,select(x:'a. t)))
(r:hprod(). ,(f:hnum 'a. (n:hnum. ,,n))))))
