Redo coinductive amortized analysis synthetically

[HarrisonGrodin]

Big idea:

• [x] Change dequeue type from F (prod⁺ (maybe E) (U (queue X))) to maybe E ⋉ queue X.
  • Cost propagates into the right component.
  • The equivalence principle ≈ is then the natural choice of bisimulation for queue X; by construction, no cost goes to computing the value component.
• [x] Change ψ output type from F A to A ⋉ X.