induction h using Relation.ReflTransGen.head_induction_on
α : Type u_1
x z : α
r : α → α → Prop
h : Relation.ReflTransGen r x z
⊢ ∃ n ys, x = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
case refl
α : Type u_1
x z : α
r : α → α → Prop
⊢ ∃ n ys, z = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)

case head
α : Type u_1
x z : α
r : α → α → Prop
a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : Relation.ReflTransGen r c✝ z
a✝ : ∃ n ys, c✝ = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)
⊢ ∃ n ys, a✝¹ = ys.head ∧ z = ys.last ∧ ∀ (i : Fin n), r (ys.get i.castSucc) (ys.get i.succ)