2 lines
98 B
Text
2 lines
98 B
Text
theorem ex : ∀ {n : Nat} {i j : Fin n}, i = j → i.val = j.val :=
|
|
fun {n} {i j} h => h ▸ rfl
|