Get the varname field from a indname-result.
(indname-result->varname x) → varname
This is an ordinary field accessor created by defprod.
Function:
(defun indname-result->varname$inline (x) (declare (xargs :guard (indname-result-p x))) (declare (xargs :guard t)) (let ((__function__ 'indname-result->varname)) (declare (ignorable __function__)) (mbe :logic (b* ((x (and t x))) (svar-fix (car x))) :exec (car x))))
Theorem:
(defthm svar-p-of-indname-result->varname (b* ((varname (indname-result->varname$inline x))) (svar-p varname)) :rule-classes :rewrite)
Theorem:
(defthm indname-result->varname$inline-of-indname-result-fix-x (equal (indname-result->varname$inline (indname-result-fix x)) (indname-result->varname$inline x)))
Theorem:
(defthm indname-result->varname$inline-indname-result-equiv-congruence-on-x (implies (indname-result-equiv x x-equiv) (equal (indname-result->varname$inline x) (indname-result->varname$inline x-equiv))) :rule-classes :congruence)