intro k hk
case 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) (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
case 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
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