Theorem: bitvec_AndOrXor_716 (Eval/bitvec_AndOrXor_716.lean)

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

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