Generate the hints to prove the theorem that relates the old and new function, when some result of a multi-valued function is being transformed.
(isodata-gen-old-to-new-thm-hints-mres old-to-new-lemma-name old-to-list-of-mv-nth-name) → hints
Function:
(defun isodata-gen-old-to-new-thm-hints-mres (old-to-new-lemma-name old-to-list-of-mv-nth-name) (declare (xargs :guard (and (symbolp old-to-new-lemma-name) (symbolp old-to-list-of-mv-nth-name)))) (let ((__function__ 'isodata-gen-old-to-new-thm-hints-mres)) (declare (ignorable __function__)) (cons (cons '"Goal" (cons ':use (cons (cons old-to-new-lemma-name (cons old-to-list-of-mv-nth-name 'nil)) 'nil))) 'nil)))