intro m n k h f
case h.h.h.h
α : Type u_1
init : α
⊢ ∀ (m n k : Nat) (h : m + n = k) (f : Fin k → α → α),
    fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) =
      fold' k f init
case h.h.h.h
α : Type u_1
init : α
m n k : Nat
h : m + n = k
f : Fin k → α → α
⊢ fold'TR.loop k f m (_ : m ≤ k) (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < k) }) init) = fold' k f init