(aig-sterm-with-hint b hint) → ans
Function:
(defun aig-sterm-with-hint$inline (b hint) (declare (xargs :guard t)) (let ((__function__ 'aig-sterm-with-hint)) (declare (ignorable __function__)) (cons-with-hint b nil hint)))
Theorem:
(defthm return-type-of-aig-sterm-with-hint (b* ((ans (aig-sterm-with-hint$inline b hint))) (equal ans (aig-sterm b))) :rule-classes :rewrite)