dsimp [recComplete.aux]
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
⊢ recComplete.aux ind zero k hk = recCompleteWF ind k
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
k : Nat
hk : k ≤ zero
⊢ (ind k fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = recCompleteWF ind k