The design of recursive functions is a well-studied subject. Design methods require a specification to start with, however, when an embedding design is attempted at, it is not clear how the specification of the embedding relates to that of the initial function. We propose a method for deriving specifications of embeddings. We show how other known formal methods, such as loop derivation or program transformation, can be related to our method in a clear fashion. The use of embedding to enhance the efficiency of programs is also discussed.