case mk
n m val✝ : ℕ
isLt✝ : val✝ < n
h : succ { val := val✝, isLt := isLt✝ } ≠ 0
⊢ pred (succ { val := val✝, isLt := isLt✝ }) h = { val := val✝, isLt := isLt✝ }
n m : ℕ
i : Fin n
h : succ i ≠ 0
⊢ pred (succ i) h = i
cases i
no goals
case mk
n m val✝ : ℕ
isLt✝ : val✝ < n
h : succ { val := val✝, isLt := isLt✝ } ≠ 0
⊢ pred (succ { val := val✝, isLt := isLt✝ }) h = { val := val✝, isLt := isLt✝ }
rfl