So picture trying to take a C snippet and using it inside a JavaScript project. On top of the different language syntax, each language has different definitions

So picture trying to take a C snippet and using it inside a JavaScript project. On top of the different language syntax, each language has different definitions on equality, strings, arrays, numbers, control flow, pointers etc. so there's no simple mapping that would let you translate the C snippet into a snippet a JavaScript interpreter would understand and if you're not careful with your mapping you're going to get bugs. Similarly with theorem provers, on top of just the syntax, they each have their own definitions for equality, data structures etc. that don't have simple mappings, as well as differences in the basic proof axioms all proofs must be built on. Both specifications and their proofs won't map easily between theorem provers which you'll have to reconcile somehow.