exact hinit
case zero
α : Type u_1
motive : Nat → α → Prop
f : Nat → α → α
init : α
hinit : motive zero init
hsucc : ∀ (k : Nat) (a : α), motive (k + 1) a → motive k (f k a)
⊢ motive 0 (foldRev f zero init)
no goals