rw [BitVec.instLT]
w : Nat
x y : BitVec w
⊢ BitVec.instLT.1 x y = (decide (x.toNat < y.toNat) = true)
w : Nat
x y : BitVec w
⊢ { lt := fun x x_1 => x.toNat < x_1.toNat }.1 x y = (decide (x.toNat < y.toNat) = true)