no goals
α : Type u
β : Type v
R r : α → α → Prop
l✝ l₁ l₂ : List α
a✝ b a : α
l : List α
p : Chain R a l
⊢ Chain (fun x y => x ∈ a :: l ∧ y ∈ l ∧ R x y) a l
induction' p with _ a b l r _ IH <;> constructor <;>
  [exact ⟨mem_cons_self _ _, mem_cons_self _ _, r⟩;
  exact IH.imp fun a b ⟨am, bm, h⟩ => ⟨mem_cons_of_mem _ am, mem_cons_of_mem _ bm, h⟩]