funext k hk
case refl.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
hk : 0 ≤ zero
⊢ (fun l hl => absurd (_ : l < 0) (_ : ¬l < 0)) = fun k x => recCompleteWF ind k
case refl.h.h.h
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
hk✝ : 0 ≤ zero
k : Nat
hk : k < 0
⊢ absurd (_ : k < 0) (_ : ¬k < 0) = recCompleteWF ind k