Theorem: List.cons₂_append_inj (Lib.lean)

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