induction' n with n ih generalizing e <;> simp[*, unvector]
n e : ℕ
i : Fin n
⊢ unvector e i ≤ e
case zero
n e : ℕ
i : Fin 0
⊢ ![] ≤ e

case succ
n✝ n : ℕ
ih : ∀ (e : ℕ) (i : Fin n), unvector e i ≤ e
e : ℕ
i : Fin (n + 1)
⊢ (e.unpair.1 :> unvector e.unpair.2) i ≤ e