induction n generalizing f init motive with
| zero => exact hinit
| succ n IH =>
  rewrite [foldRev_succ]
  apply hsucc
  exact @IH (motive ∘ succ) (f ∘ succ) init hinit (fun k => hsucc (k+1))
α : Type u_1
motive : Nat → α → Prop
f : Nat → α → α
n : Nat
init : α
hinit : motive n init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive 0 (foldRev f n init)
no goals