simp at p4 p5
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 }
p4 : (fun x => init) { init := t, tail := tail } = (fun x => init) { init := qti, tail := qtt } :=
  congrArg (fun x => init) p3
p5 : (fun x => tail) { init := t, tail := tail } = (fun x => tail) { init := qti, tail := qtt } :=
  congrArg (fun x => tail) p3
⊢ t ++ List.reverse tail = qti ++ List.reverse qtt
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 }
p4 : t = qti := congrArg (fun x => init) p3
p5 : tail = qtt := congrArg (fun x => tail) p3
⊢ t ++ List.reverse tail = qti ++ List.reverse qtt