cases k
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
k : Nat
hk : k ≤ succ n
⊢ recComplete.aux ind (succ n) k hk = recCompleteWF ind k
case zero
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
⊢ recComplete.aux ind (succ n) zero hk = recCompleteWF ind zero

case succ
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
n✝ : Nat
hk : succ n✝ ≤ succ n
⊢ recComplete.aux ind (succ n) (succ n✝) hk = recCompleteWF ind (succ n✝)