Theorem: cast_unit_5' (Test/Bv/Cast.lean)

State before:
x y : BitVec 64
⊢ extractLsb 63 0 (x.append y) = extractLsb 127 64 (y ++ x)
Tactic:
bv_decide
State after:
no goals