no goals
case nil
α : Type u_1
R S : α → α → Prop
HRS : ∀ ⦃a b : α⦄, R a b → S a b
a : α
l : List α
a✝ b : α
Hab : ∀ ⦃c : α⦄, R a✝ c → S b c
⊢ Chain S b []
constructor
case cons.a
α : Type u_1
R S : α → α → Prop
HRS : ∀ ⦃a b : α⦄, R a b → S a b
a : α
l : List α
a✝¹ b✝ : α
l✝ : List α
r : R a✝¹ b✝
a✝ : Chain R b✝ l✝
ih : ∀ {b : α}, (∀ ⦃c : α⦄, R b✝ c → S b c) → Chain S b l✝
b : α
Hab : ∀ ⦃c : α⦄, R a✝¹ c → S b c
⊢ S b b✝

case cons.a
α : Type u_1
R S : α → α → Prop
HRS : ∀ ⦃a b : α⦄, R a b → S a b
a : α
l : List α
a✝¹ b✝ : α
l✝ : List α
r : R a✝¹ b✝
a✝ : Chain R b✝ l✝
ih : ∀ {b : α}, (∀ ⦃c : α⦄, R b✝ c → S b c) → Chain S b l✝
b : α
Hab : ∀ ⦃c : α⦄, R a✝¹ c → S b c
⊢ Chain S b✝ l✝
case cons
α : Type u_1
R S : α → α → Prop
HRS : ∀ ⦃a b : α⦄, R a b → S a b
a : α
l : List α
a✝¹ b✝ : α
l✝ : List α
r : R a✝¹ b✝
a✝ : Chain R b✝ l✝
ih : ∀ {b : α}, (∀ ⦃c : α⦄, R b✝ c → S b c) → Chain S b l✝
b : α
Hab : ∀ ⦃c : α⦄, R a✝¹ c → S b c
⊢ Chain S b (b✝ :: l✝)
constructor
no goals
case cons.a
α : Type u_1
R S : α → α → Prop
HRS : ∀ ⦃a b : α⦄, R a b → S a b
a : α
l : List α
a✝¹ b✝ : α
l✝ : List α
r : R a✝¹ b✝
a✝ : Chain R b✝ l✝
ih : ∀ {b : α}, (∀ ⦃c : α⦄, R b✝ c → S b c) → Chain S b l✝
b : α
Hab : ∀ ⦃c : α⦄, R a✝¹ c → S b c
⊢ S b b✝
exact Hab r
no goals
case cons.a
α : Type u_1
R S : α → α → Prop
HRS : ∀ ⦃a b : α⦄, R a b → S a b
a : α
l : List α
a✝¹ b✝ : α
l✝ : List α
r : R a✝¹ b✝
a✝ : Chain R b✝ l✝
ih : ∀ {b : α}, (∀ ⦃c : α⦄, R b✝ c → S b c) → Chain S b l✝
b : α
Hab : ∀ ⦃c : α⦄, R a✝¹ c → S b c
⊢ Chain S b✝ l✝
exact ih (@HRS _)