The formula is strange. For example, here’s a small proof fragment, where is an arbitrary goal formula:
Is the in the right premise of the loli-left rule the same as the one we started with in the conclusion?
Thinking a little bit more about my previous post about focusing:
Any unfocused sequent calculus can induce multiple viable focused calculi. Trivially, if you take one focused version you can leave off some of the focus in the conclusions. For example, the synchronous rule for tensor in focused linear logic is usually given as
but there’s nothing wrong, per se, with taking the rule to be
or the symmetric omission of focusing on the right premise, or even the degenerate