A question about "Putting Type Annotations to Work"

Hi, I am not sure whether this is the right place to ask this question: I don't understand how to compute the least upper bound of 2 (or N) substitutions in the MGI algorithm of the paper mentioned in the subject (see Figure 4 on page 10, rules (->) and (T)). Any hint is welcomed. Thanks in advance and merry Christmas, -- Diego To reply remove the 2 `x' from the address.