have : n < length α := Nat.lt_of_succ_lt ‹n.succ < length α›
α : 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 α
⊢ (f n (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).snd |||
        (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).fst,
      (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).snd <<< 1) =
    (f n (y <<< OfNat.ofNat n) ||| Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x,
      y <<< OfNat.ofNat (Nat.succ n))
α : 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 α
⊢ (f n (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).snd |||
        (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).fst,
      (Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) n (x, y)).snd <<< 1) =
    (f n (y <<< OfNat.ofNat n) ||| Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) n x,
      y <<< OfNat.ofNat (Nat.succ n))