intro
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
⊢ ⟨i + 1, hi⟩.toIndView = IndView.zero → IndView.zero.toFin = ⟨i + 1, hi⟩
case mp
n✝¹ n✝ : Nat
i✝ : Fin n✝
j : Fin.IndView n✝
n i : Nat
hi : i + 1 < n + 1
a✝ : ⟨i + 1, hi⟩.toIndView = IndView.zero
⊢ IndView.zero.toFin = ⟨i + 1, hi⟩