case refl
α : Type u_1
β : Type ?u.30291
γ : Type ?u.30294
δ : Type ?u.30297
r : α → α → Prop
a b c d : α
r' : α → α → Prop
hr : Reflexive r
ht : Transitive r
h : ∀ (a b : α), r' a b → r a b
⊢ r a a

case tail
α : Type u_1
β : Type ?u.30291
γ : Type ?u.30294
δ : Type ?u.30297
r : α → α → Prop
a b✝ c✝ d : α
r' : α → α → Prop
hr : Reflexive r
ht : Transitive r
h : ∀ (a b : α), r' a b → r a b
b c : α
a✝ : ReflTransGen r' a b
hbc : r' b c
ih : r a b
⊢ r a c
α : Type u_1
β : Type ?u.30291
γ : Type ?u.30294
δ : Type ?u.30297
r : α → α → Prop
a b c d : α
r' : α → α → Prop
hr : Reflexive r
ht : Transitive r
h : ∀ (a b : α), r' a b → r a b
h' : ReflTransGen r' a b
⊢ r a b
induction' h' with b c _ hbc ih
no goals
case refl
α : Type u_1
β : Type ?u.30291
γ : Type ?u.30294
δ : Type ?u.30297
r : α → α → Prop
a b c d : α
r' : α → α → Prop
hr : Reflexive r
ht : Transitive r
h : ∀ (a b : α), r' a b → r a b
⊢ r a a
exact hr _
no goals
case tail
α : Type u_1
β : Type ?u.30291
γ : Type ?u.30294
δ : Type ?u.30297
r : α → α → Prop
a b✝ c✝ d : α
r' : α → α → Prop
hr : Reflexive r
ht : Transitive r
h : ∀ (a b : α), r' a b → r a b
b c : α
a✝ : ReflTransGen r' a b
hbc : r' b c
ih : r a b
⊢ r a c
exact ht ih (h _ _ hbc)