Embeddings between functional types need not be injective, and may hence loose information. This has the consequence, that the current notion of equivalent expansions for equations is not valid anymore.
This is best explained by an example. Assume that nat < int, and f, g have type int -> int. Then f = g can be expanded to an equation of sort int -> int, and to an equation of sort nat -> int by applying the embedding function emb(int -> int, nat -> int) to f and g. However, the semantics of these two equations may be different, and they should therefore not be equivalent anymore.
The problem could be solved in several ways.