Theorem: bitvec_AndOrXor_709 (Eval/bitvec_AndOrXor_709.lean)

State before:
⊢ ∀ (a b d : BitVec 64), (a &&& b == b && a &&& d == d) = (a &&& (b ||| d) == b ||| d)
Tactic:
intros
State after:
a✝ b✝ d✝ : BitVec 64
⊢ (a✝ &&& b✝ == b✝ && a✝ &&& d✝ == d✝) = (a✝ &&& (b✝ ||| d✝) == b✝ ||| d✝)

State before:
a✝ b✝ d✝ : BitVec 64
⊢ (a✝ &&& b✝ == b✝ && a✝ &&& d✝ == d✝) = (a✝ &&& (b✝ ||| d✝) == b✝ ||| d✝)
Tactic:
bv_decide
State after:
no goals