◇A = ∃x.[x] ⊗ □ (∀y ≥ x.[y] ⊸ A ∨ [○y])
◇A, ◇B ⊢ ◇((A∧◇B)∨(◇A∧B))
except just saying that leaves out the meaning of most of the junk in the definition, so go read the pdf anyway.
I'm actually quite pleased at the near-systematicness of this conversion of corecursion into linear token passing, I'll have to think more about that.
At various times during this stretch of thinking I thought I had a use for the "fermionically true" modality that I mentioned on twitter a while back, but sadly it doesn't appear to be necessary after all.