case refl
α : Type u_1
β : Type ?u.18068
γ : Type ?u.18071
δ : Type ?u.18074
r : α → α → Prop
a b c d : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
⊢ ReflTransGen r a c ∨ ReflTransGen r c a

case tail
α : Type u_1
β : Type ?u.18068
γ : Type ?u.18071
δ : Type ?u.18074
r : α → α → Prop
a b✝ c d✝ : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b d : α
a✝ : ReflTransGen r a b
bd : r b d
IH : ReflTransGen r b c ∨ ReflTransGen r c b
⊢ ReflTransGen r d c ∨ ReflTransGen r c d
α : Type u_1
β : Type ?u.18068
γ : Type ?u.18071
δ : Type ?u.18074
r : α → α → Prop
a b c d : α
U : Relator.RightUnique r
ab : ReflTransGen r a b
ac : ReflTransGen r a c
⊢ ReflTransGen r b c ∨ ReflTransGen r c b
induction' ab with b d _ bd IH
no goals
case refl
α : Type u_1
β : Type ?u.18068
γ : Type ?u.18071
δ : Type ?u.18074
r : α → α → Prop
a b c d : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
⊢ ReflTransGen r a c ∨ ReflTransGen r c a
exact Or.inl ac
case tail.inl
α : Type u_1
β : Type ?u.18068
γ : Type ?u.18071
δ : Type ?u.18074
r : α → α → Prop
a b✝ c d✝ : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b d : α
a✝ : ReflTransGen r a b
bd : r b d
IH : ReflTransGen r b c
⊢ ReflTransGen r d c ∨ ReflTransGen r c d

case tail.inr
α : Type u_1
β : Type ?u.18068
γ : Type ?u.18071
δ : Type ?u.18074
r : α → α → Prop
a b✝ c d✝ : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b d : α
a✝ : ReflTransGen r a b
bd : r b d
IH : ReflTransGen r c b
⊢ ReflTransGen r d c ∨ ReflTransGen r c d
case tail
α : Type u_1
β : Type ?u.18068
γ : Type ?u.18071
δ : Type ?u.18074
r : α → α → Prop
a b✝ c d✝ : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b d : α
a✝ : ReflTransGen r a b
bd : r b d
IH : ReflTransGen r b c ∨ ReflTransGen r c b
⊢ ReflTransGen r d c ∨ ReflTransGen r c d
rcases IH with (IH | IH)
case tail.inl.inl
α : Type u_1
β : Type ?u.18068
γ : Type ?u.18071
δ : Type ?u.18074
r : α → α → Prop
a b✝ d✝ : α
U : Relator.RightUnique r
b d : α
a✝ : ReflTransGen r a b
bd : r b d
ac : ReflTransGen r a b
IH : ReflTransGen r b b
⊢ ReflTransGen r d b ∨ ReflTransGen r b d

case tail.inl.inr.intro.intro
α : Type u_1
β : Type ?u.18068
γ : Type ?u.18071
δ : Type ?u.18074
r : α → α → Prop
a b✝ c d✝ : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b d : α
a✝ : ReflTransGen r a b
bd : r b d
IH : ReflTransGen r b c
e : α
be : r b e
ec : ReflTransGen r e c
⊢ ReflTransGen r d c ∨ ReflTransGen r c d
case tail.inl
α : Type u_1
β : Type ?u.18068
γ : Type ?u.18071
δ : Type ?u.18074
r : α → α → Prop
a b✝ c d✝ : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b d : α
a✝ : ReflTransGen r a b
bd : r b d
IH : ReflTransGen r b c
⊢ ReflTransGen r d c ∨ ReflTransGen r c d
rcases cases_head IH with (rfl | ⟨e, be, ec⟩)
no goals
case tail.inl.inl
α : Type u_1
β : Type ?u.18068
γ : Type ?u.18071
δ : Type ?u.18074
r : α → α → Prop
a b✝ d✝ : α
U : Relator.RightUnique r
b d : α
a✝ : ReflTransGen r a b
bd : r b d
ac : ReflTransGen r a b
IH : ReflTransGen r b b
⊢ ReflTransGen r d b ∨ ReflTransGen r b d
exact Or.inr (single bd)
case tail.inl.inr.intro.intro.refl
α : Type u_1
β : Type ?u.18068
γ : Type ?u.18071
δ : Type ?u.18074
r : α → α → Prop
a b✝ c d✝ : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b d : α
a✝ : ReflTransGen r a b
bd : r b d
IH : ReflTransGen r b c
be : r b d
ec : ReflTransGen r d c
⊢ ReflTransGen r d c ∨ ReflTransGen r c d
case tail.inl.inr.intro.intro
α : Type u_1
β : Type ?u.18068
γ : Type ?u.18071
δ : Type ?u.18074
r : α → α → Prop
a b✝ c d✝ : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b d : α
a✝ : ReflTransGen r a b
bd : r b d
IH : ReflTransGen r b c
e : α
be : r b e
ec : ReflTransGen r e c
⊢ ReflTransGen r d c ∨ ReflTransGen r c d
cases U bd be
no goals
case tail.inl.inr.intro.intro.refl
α : Type u_1
β : Type ?u.18068
γ : Type ?u.18071
δ : Type ?u.18074
r : α → α → Prop
a b✝ c d✝ : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b d : α
a✝ : ReflTransGen r a b
bd : r b d
IH : ReflTransGen r b c
be : r b d
ec : ReflTransGen r d c
⊢ ReflTransGen r d c ∨ ReflTransGen r c d
exact Or.inl ec
no goals
case tail.inr
α : Type u_1
β : Type ?u.18068
γ : Type ?u.18071
δ : Type ?u.18074
r : α → α → Prop
a b✝ c d✝ : α
U : Relator.RightUnique r
ac : ReflTransGen r a c
b d : α
a✝ : ReflTransGen r a b
bd : r b d
IH : ReflTransGen r c b
⊢ ReflTransGen r d c ∨ ReflTransGen r c d
exact Or.inr (IH.tail bd)