Theorem: bitvec_AndOrXor_1683_2 (Eval/bitvec_AndOrXor_1683_2.lean)

State before:
⊢ ∀ (a b : BitVec 64), (decide (b ≤ a) || decide ((a != b) = true)) = true
Tactic:
intros
State after:
a✝ b✝ : BitVec 64
⊢ (decide (b✝ ≤ a✝) || decide ((a✝ != b✝) = true)) = true

State before:
a✝ b✝ : BitVec 64
⊢ (decide (b✝ ≤ a✝) || decide ((a✝ != b✝) = true)) = true
Tactic:
bv_decide
State after:
no goals