for any arbitrary
This unusual (but occasionally useful) proof strategy is similar to the pick-a-point proofs found in the ordered sets or ubdd libraries.
There are a couple of ways to invoke the hint. First, you might manually appeal to the theorem using a hint such as:
:use ((:functional-instance equal-by-logbitp (logbitp-hyp (lambda () my-hyps)) (logbitp-lhs (lambda () my-lhs)) (logbitp-rhs (lambda () my-rhs))))
But this can be irritating if your particular hyps, lhs, and rhs are large
or complex terms. See the equal-by-logbitp-hint computed hint, which
can generate the appropriate
(defthm logbitp-constraint (implies (and (logbitp-hyp) (natp bit) (<= bit (max (integer-length (logbitp-lhs)) (integer-length (logbitp-rhs))))) (equal (logbitp bit (logbitp-lhs)) (logbitp bit (logbitp-rhs)))))