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