generalize hn : Nat.log2RU (length α) = n
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
⊢ (Nat.fold
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
        (Nat.log2RU (length α)) (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      (Nat.log2RU (length α)) x
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ (Nat.fold
        (fun i x =>
          match x with
          | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> k, k <<< 1))
        n (x, 1)).fst =
    Nat.fold (fun i x => (x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i))
      n x