unfold maskTable
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝¹ : n < Nat.log2RU (length α)
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit maskTable[n] i = (decide (i < length α) && Nat.getBit i n)
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
n i : Nat
h : n < Array.size maskTable
this✝¹ : n < Nat.log2RU (length α)
this✝ : n < length α
this : n < 2 ^ length α
⊢ UInt.getBit (Array.ofFn fun i => bitmask (OfNat.ofNat ↑i))[n] i = (decide (i < length α) && Nat.getBit i n)