@@ -459,8 +459,7 @@ Let $M=\lambda x.(x \oplus \id)$. The following (incomplete) derivation can be b

Note that $\multiset{M}\Redo\multiset{\two\id , \two\lambda x.\id}$; while $\der\id:\dist{\multiset{\dist{\At}}\arrow\At}$, it is necessary to have weakening in order to built a derivation proving $\der\lambda x. \id: \dist{\multiset{\dist{\At}}\arrow(\multiset{\dist{\Bt}}\arrow\Bt)}$.

We are NOT obliged to consider all together all the types of the reduct, but just a subset of them. In fact the rule $\oplus$ allows to type just one component of a sum.

In order to make it more clear we could modify the text as I will write after the old one.