rewrite [foldRev_succ]
case succ
α : Type u_1
n : Nat
IH :
  ∀ {motive : Nat → α → Prop} (f : Nat → α → α) (init : α),
    motive n init → (∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)) → motive 0 (foldRev f n init)
motive : Nat → α → Prop
f : Nat → α → α
init : α
hinit : motive (succ n) init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive 0 (foldRev f (succ n) init)
case succ
α : Type u_1
n : Nat
IH :
  ∀ {motive : Nat → α → Prop} (f : Nat → α → α) (init : α),
    motive n init → (∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)) → motive 0 (foldRev f n init)
motive : Nat → α → Prop
f : Nat → α → α
init : α
hinit : motive (succ n) init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive 0 (f 0 (foldRev (f ∘ succ) n init))