Theorem: append_eq_shl_or_2 (Test/BitVec/Shift.lean)

State before:
x y : BitVec 2
⊢ x ++ y = zeroExtend 4 x <<< 2#2 ||| zeroExtend 4 y
Tactic:
sorry
State after:
no goals