induction n
α : Type u_1
r : α → α → Prop
n : ℕ
⊢ ∀ (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
case zero
α : 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

case succ
α : Type u_1
r : α → α → Prop
n✝ : ℕ
a✝ :
  ∀ (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 = ys.head ∧ z = ys.last ∧ ∀ (i : Fin (n✝ + 1)), r (ys.get i.castSucc) (ys.get i.succ)) →
      Relation.ReflTransGen r x z