constructor
α : 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
case mp
α : 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

case mpr
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ (∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := tail } = qt) →
    h = x ∧ t ++ List.reverse tail = xs