exact h0
case zero
α : Type u
motive : Nat → α → Prop
f : Fin Nat.zero → α → α
init : α
h0 : motive 0 init
hf : ∀ (i : Fin Nat.zero) (x : α), motive (↑i) x → motive (↑i + 1) (f i x)
⊢ motive Nat.zero (foldAll f init)
no goals