rfl
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 : α
⊢ f 0 (foldRev (f ∘ succ) n (f (n + 1) init)) = f 0 (foldRev (f ∘ succ) n ((f ∘ succ) n init))
no goals