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