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›]
α : 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 α
this : n < length α
⊢ y <<< OfNat.ofNat n <<< 1 = y <<< OfNat.ofNat (n + 1)
α : 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 α
this✝ : n < length α
this : toNat (OfNat.ofNat n) + toNat 1 = n + 1
⊢ y <<< OfNat.ofNat n <<< 1 = y <<< OfNat.ofNat (n + 1)