case zero =>
  dsimp [recComplete.aux]; unfold recCompleteWF
  have : k = 0 := k.eq_zero_of_le_zero hk
  cases this
  apply congrArg; funext k hk; cases hk
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
no goals