Here is a formalization (not mine) of the second recursion theorem in Agda for a somewhat more elaborate language: <a href="https://hub.darcs.net/dolio/agda-share/browse/cubical/Kleene.agda" rel="nofollow">https://hub.darcs.net/dolio/agda-share/browse/cubical/Kleene...</a>