Unnestterms crashes on comparison between related types without common supertype

[Bart Bogaerts]

Attached file: something goes wrong in unnestterms due to a comparison between variables of type Location and type Entity.

However, this equality was not in the original theory and was introduced by unnesting itself...

[Broes De Cat]

Additional details: It concerns a sort S which is a subsort of two sorts P1 and P2 without a shared parent.

Unnesting code assumes it can always introduce the parent of a sort instead of the sort itself. Other parts of the code assume the theory is well-typed: no distinct sorts are compared. E.g., equality =[P1,P2] does not even exist.

Result: problems