induction n generalizing x y
α : 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)
case zero
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
x y : α
hn : Nat.zero < length α
⊢ Nat.fold (fun i z => (f i z.snd ||| z.fst, z.snd <<< 1)) Nat.zero (x, y) =
    (Nat.fold (fun i x => f i (y <<< OfNat.ofNat i) ||| x) Nat.zero x, y <<< OfNat.ofNat Nat.zero)

case succ
α : Type
inst✝² : (n : Nat) → OfNat α n
inst✝¹ : UInt α
inst✝ : DecidableEq α
a : α
f : Nat → α → α
n✝ : Nat
n_ih✝ :
  ∀ (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✝))