That'd be great, but I think the hard part about sharing representations is that many of the proof tools are based on different underlying type theories, which make it hard to go back and forth. For example Coq is based on the calculus of inductive constructions whereas Isabelle is based on HOL. Though, I'm guessing it's possible once a type scheme is fixed. Just poking around briefly, here's an SO question and answer on some of the differences between CIC and HOL (https://stackoverflow.com/questions/30152139/what-are-the-st...)