induction n generalizing f init with
| zero => rfl
| succ n IH =>
  unfold foldRev; simp only [Nat.add, Nat.succ_eq_add_one]
  rewrite [IH]; rfl
α : Type u_1
f : Nat → α → α
n : Nat
init : α
⊢ foldRev f (n + 1) init = f 0 (foldRev (f ∘ succ) n init)
no goals