case mk
n✝ m : ℕ
C : (n : ℕ) → Fin n → Sort u_1
H0 : (n : ℕ) → C (n + 1) 0
Hs : (n : ℕ) → (i : Fin n) → C n i → C (Nat.succ n) (succ i)
n val✝ : ℕ
isLt✝ : val✝ < n
⊢ succRecOn (succ { val := val✝, isLt := isLt✝ }) H0 Hs =
    Hs n { val := val✝, isLt := isLt✝ } (succRecOn { val := val✝, isLt := isLt✝ } H0 Hs)
n✝ m : ℕ
C : (n : ℕ) → Fin n → Sort u_1
H0 : (n : ℕ) → C (n + 1) 0
Hs : (n : ℕ) → (i : Fin n) → C n i → C (Nat.succ n) (succ i)
n : ℕ
i : Fin n
⊢ succRecOn (succ i) H0 Hs = Hs n i (succRecOn i H0 Hs)
cases i
no goals
case mk
n✝ m : ℕ
C : (n : ℕ) → Fin n → Sort u_1
H0 : (n : ℕ) → C (n + 1) 0
Hs : (n : ℕ) → (i : Fin n) → C n i → C (Nat.succ n) (succ i)
n val✝ : ℕ
isLt✝ : val✝ < n
⊢ succRecOn (succ { val := val✝, isLt := isLt✝ }) H0 Hs =
    Hs n { val := val✝, isLt := isLt✝ } (succRecOn { val := val✝, isLt := isLt✝ } H0 Hs)
rfl