no goals
ι : Type ?u.11282
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ a b c : List α
x : α
⊢ x :: c = a ++ b ↔ a = [] ∧ b = x :: c ∨ ∃ a', a = x :: a' ∧ c = a' ++ b
rw [eq_comm, append_eq_cons_iff]