unfold recCompleteWF
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ (ind (k + 1) fun l hl => recComplete.aux ind n l (_ : l ≤ n)) = recCompleteWF ind (succ k)
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n : Nat
h_ind : ∀ (k : Nat) (hk : k ≤ n), recComplete.aux ind n k hk = recCompleteWF ind k
k : Nat
hk : succ k ≤ succ n
⊢ (ind (k + 1) fun l hl => recComplete.aux ind n l (_ : l ≤ n)) = ind (succ k) fun k_1 x => recCompleteWF ind k_1