induction n generalizing k
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n k : Nat
hk : k ≤ n
⊢ recComplete.aux ind n k hk = recCompleteWF ind k
case zero
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

case succ
motive : Nat → Sort u
ind : (n : Nat) → ((k : Nat) → k < n → motive k) → motive n
n✝ : Nat
n_ih✝ : ∀ (k : Nat) (hk : k ≤ n✝), recComplete.aux ind n✝ k hk = recCompleteWF ind k
k : Nat
hk : k ≤ succ n✝
⊢ recComplete.aux ind (succ n✝) k hk = recCompleteWF ind k