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