case succ n h_ind =>
  dsimp [Nat.fold]
  have : n < length α := Nat.lt_of_succ_lt ‹n.succ < length α›
  simp only [h_ind x y this]
  suffices y <<< OfNat.ofNat n <<< 1 = y <<< OfNat.ofNat (n+1)
    from congrArg _ this
  have : toNat (OfNat.ofNat (α:=α) n) + toNat (α:=α) 1 = n+1 := by
    simp only [UInt.toNat_ofNat, UInt.toNat_ofNat 1]
    have : n % 2^length α = n := Nat.mod_eq_of_lt $ calc
      n < length α := ‹_›
      _ < 2^length α := Nat.exp_lt_pow _ .refl
    have : 1 % 2^length α = 1 := Nat.mod_eq_of_lt $ calc
      1 ≤ n+1 := Nat.le_add_left ..
      _ < length α := hn
      _ < 2^length α := Nat.exp_lt_pow _ .refl
    rw [‹n % 2^length α = n›, ‹1 % 2^length α = 1›]
  calc
    y <<< OfNat.ofNat n <<< 1
      = y <<< (OfNat.ofNat n + 1) := UInt.shiftLeft_shiftLeft y (OfNat.ofNat n) 1 (this ▸ ‹n.succ < length α›)
    _ = y <<< OfNat.ofNat (n+1) := by rw [UInt.ofNat_add]
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n : Nat
h_ind :
  ∀ (x y : α),
    n < length α →
      Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y) =
        (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x, y <<< OfNat.ofNat n)
x y : α
hn : Nat.succ n < length α
⊢ Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) (Nat.succ n) (x, y) =
    (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) (Nat.succ n) x, y <<< OfNat.ofNat (Nat.succ n))
no goals