Name of the applicability condition
Function:
(defun casesplit-gen-appcond-thm-hyp-name (k) (declare (xargs :guard (natp k))) (let ((__function__ 'casesplit-gen-appcond-thm-hyp-name)) (declare (ignorable __function__)) (casesplit-gen-appcond-name-from-parts "THM" k "-HYP")))
Theorem:
(defthm symbolp-of-casesplit-gen-appcond-thm-hyp-name (b* ((name (casesplit-gen-appcond-thm-hyp-name k))) (symbolp name)) :rule-classes :rewrite)