induction h using Relation.ReflTransGen.head_induction_on
α : Type u_1
x z : α
r : α → α → Prop
h : Relation.ReflTransGen r x z
⊢ x = z ∨ x ≠ z ∧ ∃ y, x ≠ y ∧ r x y ∧ Relation.ReflTransGen r y z
case refl
α : Type u_1
x z : α
r : α → α → Prop
⊢ z = z ∨ z ≠ z ∧ ∃ y, z ≠ y ∧ r z y ∧ Relation.ReflTransGen r y z

case head
α : Type u_1
x z : α
r : α → α → Prop
a✝¹ c✝ : α
h'✝ : r a✝¹ c✝
h✝ : Relation.ReflTransGen r c✝ z
a✝ : c✝ = z ∨ c✝ ≠ z ∧ ∃ y, c✝ ≠ y ∧ r c✝ y ∧ Relation.ReflTransGen r y z
⊢ a✝¹ = z ∨ a✝¹ ≠ z ∧ ∃ y, a✝¹ ≠ y ∧ r a✝¹ y ∧ Relation.ReflTransGen r y z