e'iter = poly1 (\t zero -> eλ (t --> t) (\step -> eλ t'nat (\nat -> (nat %:: t) .: zero .: step)))

e'const :: Exp
e'const = eλ t'nat (\nat -> e'succ .: e'zero)

-- | basic iteration example
-- >>> typecheck e'count == t'nat
-- True