apply Nat.fold_congr
α : 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) =
    Nat.fold
      (fun i x =>
        match x with
        | (x, snd) =>
          ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
            1 <<< OfNat.ofNat (i + 1)))
      n (x, 1)
case zero
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ (match (x, 1) with
    | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat 0)) + (x &&& bitmask (OfNat.ofNat 0)) >>> k, k <<< 1)) =
    match (x, 1) with
    | (x, snd) =>
      ((x &&& ~~~bitmask (OfNat.ofNat 0)) + (x &&& bitmask (OfNat.ofNat 0)) >>> (1 <<< OfNat.ofNat 0),
        1 <<< OfNat.ofNat (0 + 1))

case succ
α : Type
inst✝¹ : (n : Nat) → OfNat α n
inst✝ : UInt α
x : α
n : Nat
hn : Nat.log2RU (length α) = n
⊢ ∀ (i : Nat) (a : α × α),
    i + 1 < n →
      (match
          match a with
          | (x, snd) =>
            ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
              1 <<< OfNat.ofNat (i + 1)) with
        | (x, k) => ((x &&& ~~~bitmask (OfNat.ofNat (i + 1))) + (x &&& bitmask (OfNat.ofNat (i + 1))) >>> k, k <<< 1)) =
        match
          match a with
          | (x, snd) =>
            ((x &&& ~~~bitmask (OfNat.ofNat i)) + (x &&& bitmask (OfNat.ofNat i)) >>> (1 <<< OfNat.ofNat i),
              1 <<< OfNat.ofNat (i + 1)) with
        | (x, snd) =>
          ((x &&& ~~~bitmask (OfNat.ofNat (i + 1))) +
              (x &&& bitmask (OfNat.ofNat (i + 1))) >>> (1 <<< OfNat.ofNat (i + 1)),
            1 <<< OfNat.ofNat (i + 1 + 1))