other
(in-package "ACL2")
other
(verify-termination all-fnnames1 (declare (xargs :verify-guards nil)))
true-listp-all-fnnamestheorem
(defthm true-listp-all-fnnames (implies (true-listp acc) (true-listp (all-fnnames1 flg x acc))))
other
(verify-guards all-fnnames1)