cases hk
case h.h.h
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
k : Nat
hk : k < 0
⊢ absurd hk (_ : ¬k < 0) = recCompleteWF ind k
no goals