Theorem: QueueData.nonEmptyAppend (Advent/Queue.lean)

State before:
α : Type u_1
xs ys : List α
x : α
p : xs ++ x :: ys = []
⊢ False
Tactic:
cases xs <;> simp at p
State after:
no goals