cases q.init <;> cases q.tail <;> simp
α : Type u_1
q : QueueData α
⊢ init ++ List.reverse tail = [] ↔
    (match init with
      | x :: xs => some (x, { init := xs, tail := tail })
      | [] =>
        match List.reverse tail with
        | x :: xs => some (x, { init := xs, tail := [] })
        | [] => none) =
      none
case nil.cons
α : Type u_1
q : QueueData α
head✝ : α
tail✝ : List α
⊢ List.reverse tail✝ ++ [head✝] = [] ↔
    (match List.reverse tail✝ ++ [head✝] with
      | x :: xs => some (x, { init := xs, tail := [] })
      | [] => none) =
      none