T |- T
might hold in linear K in the weather report, but it definitely doesn't: the  on the right wants the context to be empty right now.
Dealing with this finally reconciled the apparent gross asymmetry between pfenning-davies box and diamond. To make sure this doesn't hold in my encoding, box needs a funny side-condition just like diamond and everything is symmetric and beautiful again. Started writing it up a little bit here.