rw [p2, ← p1]
case mpr.intro.intro.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p2 : h = x
qti qtt : List α
p1 : init ++ List.reverse tail = xs
p3 : { init := t, tail := tail } = { init := qti, tail := qtt }
⊢ h = x ∧ t ++ List.reverse tail = xs
case mpr.intro.intro.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p2 : h = x
qti qtt : List α
p1 : init ++ List.reverse tail = xs
p3 : { init := t, tail := tail } = { init := qti, tail := qtt }
⊢ x = x ∧ t ++ List.reverse tail = init ++ List.reverse tail