(in-package "ACL2")
(defun f (x) x)