Handle embeddings more restrictively in GUI

[SReichelt]

Architecturally, embeddings essentially "fuse" two types. Since the natural numbers are embedded into several other number systems, all of these number systems are treated as one, resulting in lots of options that do not really make much sense (although they are technically valid).

This should be handled more restrictively in two ways:

• When determining valid options for an argument placeholder, embeddings of a possible option should not be followed by default, as described in More explicit type constraints for arguments #60. In the library tree dialog, there needs to be an option to "also consider embedded subsets", i.e. to turn off this restriction. The restriction should never be applied to variables, as no such option is available there.
• In addition, a more general restriction should always be applied: Placeholders should never be filled in a way that forces both the placeholder and all other terms that are type-checked together with it to follow embeddings. However, since following embeddings is a crucial part of type checking, this restriction probably needs to be checked after embeddings have already been followed in all terms that are type-checked together. One way to accomplish this would be to record and compare the list of constructions encountered when following embeddings: The list containing the checked placeholder should either contain or be contained in one of the other lists.

Somewhat related to #64, as that issue also deals with more restrictive type checking of placeholders.