no goals
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a✝ b✝ a b : α
l₁ l₂ : List α
⊢ Chain R a (l₁ ++ b :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ Chain R b l₂
induction' l₁ with x l₁ IH generalizing a <;>
  simp only [*, nil_append, cons_append, Chain.nil, chain_cons, and_true_iff, and_assoc]