(in-package "ACL2")
(verify-termination doublet-listp)
(verify-termination defstobj-fnname)
(verify-termination defstobj-fnname-key2)