[logic-ml] proof theory of skew monoidal categories