Theorem: bitvec_AndOrXor_2367 (Eval/bitvec_AndOrXor_2367.lean)

State before:
⊢ ∀ (A C1 op1 : BitVec 64), A ||| C1 ||| op1 = A ||| op1 ||| C1
Tactic:
intros
State after:
A✝ C1✝ op1✝ : BitVec 64
⊢ A✝ ||| C1✝ ||| op1✝ = A✝ ||| op1✝ ||| C1✝

State before:
A✝ C1✝ op1✝ : BitVec 64
⊢ A✝ ||| C1✝ ||| op1✝ = A✝ ||| op1✝ ||| C1✝
Tactic:
bv_decide
State after:
no goals