Function:
(defun bird-in-some-hole (bird hole) (declare (xargs :guard (and (natp bird) (natp hole)))) (let ((__function__ 'bird-in-some-hole)) (declare (ignorable __function__)) (b* (((when (zp hole)) nil) (hole (- hole 1))) (cons (bird-in-hole bird hole) (bird-in-some-hole bird hole)))))
Theorem:
(defthm lit-listp-of-bird-in-some-hole (b* ((clause (bird-in-some-hole bird hole))) (lit-listp clause)) :rule-classes :rewrite)