The transformation from BCInf to their types
The number of internal nodes in the type of a BCInf term is the same as the number of internal nodes in the BCInf term.
 For each lambdanode, draw an arc from its leaf, through the lambdanode, and to its child.

For each applynode, draw an arc from its right child, through its left child, and to the applynode.