simp
case refl
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n : α
i : Nat
hn : toNat n < length α
this✝¹ : 2 ^ toNat n < 2 ^ length α
this✝ : 1 < 2 ^ length α
h_ind : i ≤ length α → UInt.getBit (bitmask.aux n i) i = (decide (i < i) && Nat.getBit i (toNat n))
hk : Nat.succ i ≤ length α
this : i < 2 ^ length α
hge : i ≥ i
⊢ (decide (i < i) != decide (i = i) && Nat.getBit i (toNat n)) = (decide (i < Nat.succ i) && Nat.getBit i (toNat n))
no goals