intro f n y hn
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a x : α
⊢ ∀ (f : Nat → α → α) (n : Nat) (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)
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a x : α
f : Nat → α → α
n : Nat
y : α
hn : 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)