dsimp [UInt.getBit]
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ UInt.getBit 1 i = decide (i = 0)
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
i : Nat
hpos : length α > 0
⊢ Nat.getBit (toNat 1) i = decide (i = 0)