(bed-op-arg2) → op
Function:
(defun bed-op-arg2$inline nil (declare (xargs :guard t)) (let ((__function__ 'bed-op-arg2)) (declare (ignorable __function__)) 10))
Theorem:
(defthm bed-op-p-of-bed-op-arg2 (b* ((op (bed-op-arg2$inline))) (bed-op-p op)) :rule-classes :rewrite)
Theorem:
(defthm bed-op-eval-of-arg2 (equal (bed-op-eval (bed-op-arg2) x y) (bfix y)))