simp
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ h :: t ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match h :: t 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)
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ h = x ∧ t ++ List.reverse tail = xs ↔ ∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := tail } = qt