simp only [Fin.castSucc_zero, Vector.get_zero, Fin.succ_zero_eq_one] at steprel
case h.left
α : 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
y : α := ys.tail.head
steprel : r (ys.get (Fin.castSucc 0)) (ys.get (Fin.succ 0))
⊢ r x y
case h.left
α : 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
y : α := ys.tail.head
steprel : r ys.head (ys.get 1)
⊢ r x y