generalize p : q.tail.reverse = tr
case nil
α : Type u_1
q : QueueData α
x : α
xs : List α
⊢ [] ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match [] 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)

case cons
α : Type u_1
q : QueueData α
x : α
xs : List α
head✝ : α
tail✝ : List α
⊢ head✝ :: tail✝ ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match head✝ :: tail✝ 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)
case nil
α : Type u_1
q : QueueData α
x : α
xs tr : List α
p : List.reverse tail = tr
⊢ [] ++ tr = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match [] with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match tr with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)

case cons
α : Type u_1
q : QueueData α
x : α
xs : List α
head✝ : α
tail✝ : List α
⊢ head✝ :: tail✝ ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match head✝ :: tail✝ 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)