Theorem: cast_unit_4 (Test/Bv/Cast.lean)

State before:
x y : BitVec 32
⊢ extractLsb 32 0 (zeroExtend 64 x) = extractLsb 32 0 (zeroExtend 64 y) → x = y
Tactic:
bv_decide
State after:
no goals