refine dfold_induction (α := fun i => i ≤ n → α) (motive := fun i a => (h : i ≤ n) → motive i (a h)) _ n (fun _ => init) (fun _ => zero) ?_ .refl
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
⊢ motive n (dfold (fun i x hi => f { val := i, isLt := hi } (x (_ : i ≤ n))) n (fun x => init) (_ : Nat.le n n))
α : Type u
motive : Nat → α → Prop
n : Nat
f : Fin n → α → α
init : α
zero : motive 0 init
succ : ∀ (i : Nat) (hi : i < n) (a : α), motive i a → motive (i + 1) (f { val := i, isLt := hi } a)
⊢ ∀ (n_1 : Nat) (a : (fun i => i ≤ n → α) n_1),
    (fun i a => ∀ (h : i ≤ n), motive i (a h)) n_1 a →
      (fun i a => ∀ (h : i ≤ n), motive i (a h)) (n_1 + 1) fun hi => f { val := n_1, isLt := hi } (a (_ : n_1 ≤ n))