case mk
α : Type u
n val✝ : ℕ
isLt✝ : val✝ < n
⊢ { val := ↑{ val := val✝, isLt := isLt✝ }, isLt := (_ : ↑{ val := val✝, isLt := isLt✝ } < n) } =
    { val := val✝, isLt := isLt✝ }
α : Type u
n : ℕ
a : Fin n
⊢ { val := ↑a, isLt := (_ : ↑a < n) } = a
cases a
no goals
case mk
α : Type u
n val✝ : ℕ
isLt✝ : val✝ < n
⊢ { val := ↑{ val := val✝, isLt := isLt✝ }, isLt := (_ : ↑{ val := val✝, isLt := isLt✝ } < n) } =
    { val := val✝, isLt := isLt✝ }
rfl