perhaps proof assistants should support multiple formalisms (think MLTT, ZFC, etc), letting you work in whichever is convenient at the moment by compiling your proofs between them as necessary
If you have a fediverse account, you can quote this note from your own instance. Search https://donotsta.re/objects/a7904b9f-7c89-40e9-a96b-cbee15ebc7e4 on your instance and quote it. (Note that quoting is not supported in Mastodon.)