simp [*]
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
⊢ h = x ∧ t = xs
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
⊢ t = xs