rw [← p3, ← p4] at p1
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 : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1.right.right
p3 : t = qi := congrArg (fun x => init) p2
p4 : [] = qt := congrArg (fun x => tail) p2
⊢ 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✝ : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p1 : t ++ List.reverse [] = xs ∧ h = x ∧ { init := t, tail := [] } = { init := t, tail := [] }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1✝.right.right
p3 : t = qi := congrArg (fun x => init) p2
p4 : [] = qt := congrArg (fun x => tail) p2
⊢ t = xs