apply congrArg
case h.h.h.h.succ.refl
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (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
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
          (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) a)) =
      fold' (m + n + 1) f a
⊢ fold'TR.loop (succ (m + n)) f m (_ : m ≤ succ (m + n))
      (f { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) }
        (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < succ (m + n)) }) init)) =
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
      (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
        (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) init))
case h.h.h.h.succ.refl.h
α : Type u_1
m : Nat
IH :
  ∀ (init : α) (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
init : α
n : Nat
h : succ m + n = succ (m + n)
f : Fin (succ (m + n)) → α → α
this :
  ∀ (a : α),
    fold'TR.loop (m + n + 1) f m (_ : m ≤ m + n + 1)
        (f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
          (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) a)) =
      fold' (m + n + 1) f a
⊢ f { val := succ (m + n) - (m + 1), isLt := (_ : succ (m + n) - (m + 1) < succ (m + n)) }
      (fold' n (fun i => f { val := i.val, isLt := (_ : i.val < succ (m + n)) }) init) =
    f { val := (Fin.last n).val, isLt := (_ : (Fin.last n).val < m + n + 1) }
      (fold' n ((fun i => f { val := i.val, isLt := (_ : i.val < m + n + 1) }) ∘ Fin.castSucc) init)