Theorem: List.cons_append_inj (Lib.lean)

State before:
α : Type u_1
a : α
x y z : List α
⊢ a :: (y ++ x) = z ++ x ↔ a :: y = z
Tactic:
simp [-List.cons_append, (List.cons_append _ _ _).symm]
State after:
no goals