simp only [fold'TR.loop, zero_eq]
case h.h.h.h.zero.refl
α : Type u_1
init : α
n : Nat
h : zero + n = n
f : Fin n → α → α
⊢ fold'TR.loop n f zero (_ : zero ≤ n) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < n) }) init) =
    fold' n f init
no goals