unfold foldRev
case succ
α : Type u_1
n : Nat
IH : ∀ (f : Nat → α → α) (init : α), foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
f : Nat → α → α
init : α
⊢ foldRev f (succ n + 1) init = f 0 (foldRev (f ∘ succ) (succ n) init)
case succ
α : Type u_1
n : Nat
IH : ∀ (f : Nat → α → α) (init : α), foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
f : Nat → α → α
init : α
⊢ foldRev f (Nat.add (succ n) 0) (f (Nat.add (succ n) 0) init) = f 0 (foldRev (f ∘ succ) n ((f ∘ succ) n init))