Theorem: Fin.val_ndrec (GMLInit/Data/Fin/Basic.lean)

State before:
n m : Nat
i : Fin n
h : n = m
⊢ ↑(h ▸ i) = ↑i
Tactic:
cases h
State after:
case refl
n : Nat
i : Fin n
⊢ ↑(⋯ ▸ i) = ↑i

State before:
case refl
n : Nat
i : Fin n
⊢ ↑(⋯ ▸ i) = ↑i
Tactic:
rfl
State after:
no goals