15. Transporting derivations between languages

Changing a proof language can introduce auxiliary claims, replace a rule by a derivation, or merge claims that the source language distinguishes. A dictionary of names does not justify these changes. A translation must preserve the inference being used. We distinguish forward proof transport, reflection of old consequences, and preservation of a protected request.