Post #1782119

@mdhughes Aside, ACL2 has support for limited second order logic, but it works by reinterpreting apply$ by basically inlining the functions being applied. Similarly, it supports iteration (loop$) rather than just recursion.