Generate the hints to prove
(isodata-gen-new-to-old-thm-hints-mres new-to-old-lemma-name new-to-list-of-mv-nth-name) → hints
Function:
(defun isodata-gen-new-to-old-thm-hints-mres (new-to-old-lemma-name new-to-list-of-mv-nth-name) (declare (xargs :guard (and (symbolp new-to-old-lemma-name) (symbolp new-to-list-of-mv-nth-name)))) (let ((__function__ 'isodata-gen-new-to-old-thm-hints-mres)) (declare (ignorable __function__)) (cons (cons '"Goal" (cons ':use (cons (cons new-to-old-lemma-name (cons new-to-list-of-mv-nth-name 'nil)) 'nil))) 'nil)))