α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b✝ : α
inst✝ : IsTrans α R
a b : α
l : List α
h : R a b
hb : Chain R b l
⊢ ∀ (a_1 : α), a_1 ∈ l → R a a_1
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b✝ : α
inst✝ : IsTrans α R
a b : α
l : List α
h : R a b
hb : Chain R b l
⊢ ∀ (a' : α), a' ∈ b :: l → R a a'
simp only [mem_cons, forall_eq_or_imp, h, true_and_iff]
no goals
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b✝ : α
inst✝ : IsTrans α R
a b : α
l : List α
h : R a b
hb : Chain R b l
⊢ ∀ (a_1 : α), a_1 ∈ l → R a a_1
exact fun c hc => _root_.trans h (rel_of_pairwise_cons hb.pairwise hc)