case zero =>
  rintro x z ys ⟨x_is_head, z_is_last, _⟩
  have : x = z := by
    subst_eqs
    simp_all [Vector.head, Vector.last, Fin.last]
  rw [this]
α : Type u_1
r : α → α → Prop
⊢ ∀ (x z : α) (ys : Vector α (Nat.succ 0)),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin 0), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
no goals