simp_all [Vector.head, Vector.last, Fin.last]
case refl.refl
α : Type u_1
r : α → α → Prop
ys : Vector α (Nat.succ 0)
right✝ : ∀ (i : Fin 0), r (ys.get i.castSucc) (ys.get i.succ)
⊢ ys.head = ys.last
no goals