unfold maskTable
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ (Array.foldl
        (fun x mask =>
          match x with
          | (x, k) => ((x &&& ~~~mask) + (x &&& mask) >>> k, k <<< 1))
        (x, 1) maskTable 0 (Array.size maskTable)).fst =
    (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ (Array.foldl
        (fun x mask =>
          match x with
          | (x, k) => ((x &&& ~~~mask) + (x &&& mask) >>> k, k <<< 1))
        (x, 1) (Array.ofFn fun i => bitmask (OfNat.ofNat ↑i)) 0
        (Array.size (Array.ofFn fun i => bitmask (OfNat.ofNat ↑i)))).fst =
    (Fin.foldAll
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat ↑i)) + (x &&& bitmask (OfNat.ofNat ↑i)) >>> k, k <<< 1))
        (x, 1)).fst