α : Type u_1
β : Type ?u.17848
γ : Type ?u.17851
δ : Type ?u.17854
r : α → α → Prop
a b c d : α
⊢ (a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b) → ReflTransGen r a b
α : Type u_1
β : Type ?u.17848
γ : Type ?u.17851
δ : Type ?u.17854
r : α → α → Prop
a b c d : α
⊢ ReflTransGen r a b ↔ a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b
use cases_head
case inl
α : Type u_1
β : Type ?u.17848
γ : Type ?u.17851
δ : Type ?u.17854
r : α → α → Prop
a c d : α
⊢ ReflTransGen r a a

case inr.intro.intro
α : Type u_1
β : Type ?u.17848
γ : Type ?u.17851
δ : Type ?u.17854
r : α → α → Prop
a b c✝ d c : α
hac : r a c
hcb : ReflTransGen r c b
⊢ ReflTransGen r a b
α : Type u_1
β : Type ?u.17848
γ : Type ?u.17851
δ : Type ?u.17854
r : α → α → Prop
a b c d : α
⊢ (a = b ∨ ∃ c, r a c ∧ ReflTransGen r c b) → ReflTransGen r a b
rintro (rfl | ⟨c, hac, hcb⟩)
no goals
case inl
α : Type u_1
β : Type ?u.17848
γ : Type ?u.17851
δ : Type ?u.17854
r : α → α → Prop
a c d : α
⊢ ReflTransGen r a a
rfl
no goals
case inr.intro.intro
α : Type u_1
β : Type ?u.17848
γ : Type ?u.17851
δ : Type ?u.17854
r : α → α → Prop
a b c✝ d c : α
hac : r a c
hcb : ReflTransGen r c b
⊢ ReflTransGen r a b
exact head hac hcb