Calculate lemmas instances for the lifting theorem.
(lift-thm-omap-keys-lemma-instances vars witness) → lemma-instances
We generate one lemma instance for each variable passed as input. The lemma is the same for all instances.
Function:
(defun lift-thm-omap-keys-lemma-instances (vars witness) (declare (xargs :guard (string-listp vars))) (let ((__function__ 'lift-thm-omap-keys-lemma-instances)) (declare (ignorable __function__)) (cond ((endp vars) nil) (t (cons (cons ':instance (cons 'lift-rule-omap-in-to-in-of-keys (cons (cons 'key (cons (car vars) 'nil)) (cons (cons 'map (cons witness 'nil)) 'nil)))) (lift-thm-omap-keys-lemma-instances (cdr vars) witness))))))
Theorem:
(defthm true-listp-of-lift-thm-omap-keys-lemma-instances (b* ((lemma-instances (lift-thm-omap-keys-lemma-instances vars witness))) (true-listp lemma-instances)) :rule-classes :rewrite)