cases ys using Vector.inductionOn
α : 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 : α
ys : Vector α (n + 1).succ
x_is_head : x = ys.head
z_is_last : z = ys.last
steprel : ∀ (i : Fin (n + 1)), r (ys.get i.castSucc) (ys.get i.succ)
y : α := ys.tail.head
⊢ ys.tail.last = ys.last
case h_cons
α : 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 x✝ : α
w✝ : Vector α (n + 1)
x_is_head : x = (x✝ ::ᵥ w✝).head
z_is_last : z = (x✝ ::ᵥ w✝).last
steprel : ∀ (i : Fin (n + 1)), r ((x✝ ::ᵥ w✝).get i.castSucc) ((x✝ ::ᵥ w✝).get i.succ)
y : α := (x✝ ::ᵥ w✝).tail.head
a✝ : (n + 1).succ = n + 1 → HEq (x✝ ::ᵥ w✝) w✝ → (x✝ ::ᵥ w✝).tail.last = (x✝ ::ᵥ w✝).last
⊢ (x✝ ::ᵥ w✝).tail.last = (x✝ ::ᵥ w✝).last