<pre>
(\y. y <b>x<sub>1</sub></b>) x<sub>1</sub> [x->I, ...]<sub>1</sub> [x->0]<sub>2</sub>
-y x<sub>1</sub> [y->I, x->I, ...]<sub>1</sub> [x->0]<sub>2</sub>
+y <b>x<sub>1</sub></b> [y->I, x->I, ...]<sub>1</sub> [x->0]<sub>2</sub>
I I
I
</pre>
<pre>
(\y. y <b>x<sub>2</sub></b>) x<sub>1</sub> [x->I, ...]<sub>1</sub> [x->0]<sub>2</sub>
-y x<sub>2</sub> [y->I, x->I, ...]<sub>1</sub> [x->0]<sub>2</sub>
+y <b>x<sub>2</sub></b> [y->I, x->I, ...]<sub>1</sub> [x->0]<sub>2</sub>
I 0
0
</pre>