simp [toList, pull]
α : Type u_1
q : QueueData α
x : α
xs : List α
⊢ toList q = x :: xs ↔ ∃ qt, toList qt = xs ∧ pull q = some (x, qt)
α : Type u_1
q : QueueData α
x : α
xs : List α
⊢ init ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match init with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match List.reverse tail with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)