case mk
n✝ m n val✝ : ℕ
isLt✝ : val✝ < n
h : ↑{ val := val✝, isLt := isLt✝ } < n
⊢ castLT (↑castSucc { val := val✝, isLt := isLt✝ }) h = { val := val✝, isLt := isLt✝ }
n✝ m n : ℕ
a : Fin n
h : ↑a < n
⊢ castLT (↑castSucc a) h = a
cases a
no goals
case mk
n✝ m n val✝ : ℕ
isLt✝ : val✝ < n
h : ↑{ val := val✝, isLt := isLt✝ } < n
⊢ castLT (↑castSucc { val := val✝, isLt := isLt✝ }) h = { val := val✝, isLt := isLt✝ }
rfl