cases IH_b_z
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
IH_b_z : b = z ∨ b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
a_neq_b : ¬a = b
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z
case inl
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
h✝ : b = z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z

case inr
α : Type u_1
x z : α
r : α → α → Prop
a b : α
a_r_b : r a b
b_r_z : Relation.ReflTransGen r b z
a_neq_b : ¬a = b
h✝ : b ≠ z ∧ ∃ y, b ≠ y ∧ r b y ∧ Relation.ReflTransGen r y z
⊢ a = z ∨ a ≠ z ∧ ∃ y, a ≠ y ∧ r a y ∧ Relation.ReflTransGen r y z