simp [isEmpty, toList, List.isEmpty]
α : Type u_1
q : QueueData α
⊢ isEmpty q = true ↔ toList q = []
α : 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 = []