constructor
α : Type u_1
q : QueueData α
h : α
t : List α
⊢ List.reverse t ++ [h] = [] ↔
    (match List.reverse t ++ [h] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none
case mp
α : Type u_1
q : QueueData α
h : α
t : List α
⊢ List.reverse t ++ [h] = [] →
    (match List.reverse t ++ [h] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none

case mpr
α : Type u_1
q : QueueData α
h : α
t : List α
⊢ (match List.reverse t ++ [h] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none →
    List.reverse t ++ [h] = []