no goals
α : Type u
β : Type v
R r : α → α → Prop
l l₁✝ l₂✝ : List α
a b✝ b c : α
l₁ l₂ : List α
⊢ Chain' R (l₁ ++ b :: c :: l₂) ↔ Chain' R (l₁ ++ [b]) ∧ R b c ∧ Chain' R (c :: l₂)
rw [chain'_split, chain'_cons]