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
hk : zero ≤ succ n
⊢ (ind 0 fun k hk => absurd hk (_ : ¬k < 0)) = recCompleteWF ind 0
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
hk : zero ≤ succ n
⊢ (ind 0 fun k hk => absurd hk (_ : ¬k < 0)) = ind 0 fun k x => recCompleteWF ind k