no goals
ι : Type ?u.10352
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ a b c : List α
x : α
⊢ a ++ b = x :: c ↔ a = [] ∧ b = x :: c ∨ ∃ a', a = x :: a' ∧ c = a' ++ b
cases a <;>
  simp only [and_assoc, @eq_comm _ c, nil_append, cons_append, cons.injEq, true_and_iff,
    false_and_iff, exists_false, false_or_iff, or_false_iff, exists_and_left, exists_eq_left']