α : Type u_1
β : Type ?u.24015
γ : Type ?u.24018
δ : Type ?u.24021
r : α → α → Prop
a b c d : α
h : ∀ (b : α), ¬r a b
⊢ (a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b) ↔ b = a
α : Type u_1
β : Type ?u.24015
γ : Type ?u.24018
δ : Type ?u.24021
r : α → α → Prop
a b c d : α
h : ∀ (b : α), ¬r a b
⊢ ReflTransGen r a b ↔ b = a
rw [cases_head_iff]
no goals
α : Type u_1
β : Type ?u.24015
γ : Type ?u.24018
δ : Type ?u.24021
r : α → α → Prop
a b c d : α
h : ∀ (b : α), ¬r a b
⊢ (a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b) ↔ b = a
simp [h, eq_comm]