case h_cons y ys hyp =>
  cases ys using Vector.inductionOn
  rfl
α : Type u_1
r : α → α → Prop
n : ℕ
IH :
  ∀ (x z : α) (ys : Vector α n.succ),
    (x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)) → Relation.ReflTransGen r x z
x z y✝ : α
ys : Vector α (n + 1)
x_is_head : x = (y✝ ::ᵥ ys).head
z_is_last : z = (y✝ ::ᵥ ys).last
steprel : ∀ (i : Fin (n + 1)), r ((y✝ ::ᵥ ys).get i.castSucc) ((y✝ ::ᵥ ys).get i.succ)
y : α := (y✝ ::ᵥ ys).tail.head
hyp : (n + 1).succ = n + 1 → HEq (y✝ ::ᵥ ys) ys → (y✝ ::ᵥ ys).tail.last = (y✝ ::ᵥ ys).last
⊢ (y✝ ::ᵥ ys).tail.last = (y✝ ::ᵥ ys).last
no goals