case mk
n m : ℕ
C : Fin (n + 1) → Sort u_1
h0 : C 0
hs : (i : Fin n) → C (↑castSucc i) → C (succ i)
val✝ : ℕ
isLt✝ : val✝ < n
⊢ (fun i => induction h0 hs i) (succ { val := val✝, isLt := isLt✝ }) =
    hs { val := val✝, isLt := isLt✝ } (induction h0 hs (↑castSucc { val := val✝, isLt := isLt✝ }))
n m : ℕ
C : Fin (n + 1) → Sort u_1
h0 : C 0
hs : (i : Fin n) → C (↑castSucc i) → C (succ i)
i : Fin n
⊢ (fun i => induction h0 hs i) (succ i) = hs i (induction h0 hs (↑castSucc i))
cases i
no goals
case mk
n m : ℕ
C : Fin (n + 1) → Sort u_1
h0 : C 0
hs : (i : Fin n) → C (↑castSucc i) → C (succ i)
val✝ : ℕ
isLt✝ : val✝ < n
⊢ (fun i => induction h0 hs i) (succ { val := val✝, isLt := isLt✝ }) =
    hs { val := val✝, isLt := isLt✝ } (induction h0 hs (↑castSucc { val := val✝, isLt := isLt✝ }))
rfl