intro i
case empty
α : Type u
inst✝ : DecidableEq α
⊢ ∀ (i j : Fin (size #[])), #[][↑i] = #[][↑j] → i = j
case empty
α : Type u
inst✝ : DecidableEq α
i : Fin (size #[])
⊢ ∀ (j : Fin (size #[])), #[][↑i] = #[][↑j] → i = j