no goals
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a b : α
S : α → α → Prop
H : ∀ (a b : α), R a b → S a b
l : List α
p : Chain' R l
⊢ Chain' S l
cases l <;> [trivial; exact Chain.imp H p]