<kat>
<lib><id>monosupL</id><condeqn>x @ y -> x @ y + z</condeqn><task></task><proof><LAMBDAS><id>x</id><id>y</id><id>z</id><LAMBDAP><id>P0</id><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>y</term></sub><sub><id>x</id><term>x</term></sub><sub><id>z</id><term>y + z</term></sub></APPLYS><VAR>P0</VAR><APPLYS><CONST>supL</CONST><sub><id>x</id><term>y</term></sub><sub><id>y</id><term>z</term></sub></APPLYS></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>monosupR</id><condeqn>x @ z -> x @ y + z</condeqn><task></task><proof><LAMBDAS><id>x</id><id>y</id><id>z</id><LAMBDAP><id>P1</id><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>z</term></sub><sub><id>x</id><term>x</term></sub><sub><id>z</id><term>y + z</term></sub></APPLYS><VAR>P1</VAR><APPLYS><CONST>supR</CONST><sub><id>x</id><term>y</term></sub><sub><id>y</id><term>z</term></sub></APPLYS></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
<lib><id>mono.LR</id><condeqn>x @ y -> z @ w -> x;z @ y;w</condeqn><task></task><proof><LAMBDAS><id>x</id><id>z</id><id>y</id><id>w</id><LAMBDAP><id>P3</id><id>P4</id><APPLYP><APPLYS><CONST>trans@</CONST><sub><id>y</id><term>x;w</term></sub><sub><id>x</id><term>x;z</term></sub><sub><id>z</id><term>y;w</term></sub></APPLYS><APPLYP><APPLYS><CONST>mono.L</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>z</term></sub><sub><id>z</id><term>w</term></sub></APPLYS><VAR>P4</VAR></APPLYP><APPLYP><APPLYS><CONST>mono.R</CONST><sub><id>x</id><term>x</term></sub><sub><id>y</id><term>y</term></sub><sub><id>z</id><term>w</term></sub></APPLYS><VAR>P3</VAR></APPLYP></APPLYP></LAMBDAP></LAMBDAS></proof></lib>
</kat>
