rewrite [zero_eq, Nat.zero_add] at h
case h.h.h.h.zero
α : Type u_1
init : α
n k : Nat
h : zero + n = k
f : Fin k → α → α
⊢ fold'TR.loop k f zero (_ : zero ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
    fold' k f init
case h.h.h.h.zero
α : Type u_1
init : α
n k : Nat
h✝ : zero + n = k
h : n = k
f : Fin k → α → α
⊢ fold'TR.loop k f zero (_ : zero ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
    fold' k f init