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

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