have : x = z := by
  subst_eqs
  simp_all [Vector.head, Vector.last, Fin.last]
case intro.intro
α : Type u_1
r : α → α → Prop
x z : α
ys : Vector α (Nat.succ 0)
x_is_head : x = ys.head
z_is_last : z = ys.last
right✝ : ∀ (i : Fin 0), r (ys.get i.castSucc) (ys.get i.succ)
⊢ Relation.ReflTransGen r x z
case intro.intro
α : Type u_1
r : α → α → Prop
x z : α
ys : Vector α (Nat.succ 0)
x_is_head : x = ys.head
z_is_last : z = ys.last
right✝ : ∀ (i : Fin 0), r (ys.get i.castSucc) (ys.get i.succ)
this : x = z
⊢ Relation.ReflTransGen r x z