exact IH (Nat.le_of_succ_le hk)
case h.succ.h
α : Type u
n : Nat
f : Fin (n + 1) → α → α
init : α
mot₁ : Nat → Type u := fun i => i ≤ n + 1 → α
mot₂ : Nat → Type u := fun i => i ≤ n → α
k : Nat
IH :
  ∀ (hk : k ≤ n),
    dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : Nat.le k (succ n)) =
      dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) hk
hk : succ k ≤ n
⊢ dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n + 1))) k (fun x => init) (_ : k ≤ n + 1) =
    dfold (fun i x hi => f (Fin.castSucc { val := i, isLt := hi }) (x (_ : i ≤ n))) k (fun x => init) (_ : k ≤ n)
no goals