∀ {w₁ w₂ : ℕ} (x : BitVec w₁) (y : BitVec w₂) (n : ℕ),
  x.shiftLeftRec y n =
    have shiftAmt := y &&& BitVec.twoPow w₂ n;
    match n with
    | 0 => x <<< shiftAmt
    | n.succ => x.shiftLeftRec y n <<< shiftAmt