Make tvsubst compose

[jvanbruegge]

Currently, using a nested binder_datatype does not compose the substitution functions. This is needed to e.g. substitute types in term of System F.
Prerequisites:

• Generalize the recursor to allow passive positions and mutually recursive types #10
• Allow to specify the minimum cardinal in the recursor again #18
• Make tvsubst allow passive positions #35

[jvanbruegge]

Fixed in #60