cases q.init <;> cases q.tail <;> simp
α : Type u_1
q : QueueData α
⊢ (match init with
        | [] => true
        | head :: tail => false) =
        true ∧
      (match tail with
        | [] => true
        | head :: tail => false) =
        true ↔
    init ++ List.reverse tail = []
case nil.cons
α : Type u_1
q : QueueData α
head✝ : α
tail✝ : List α
⊢ ¬List.reverse tail✝ ++ [head✝] = []