Semantic Equivalence proof support modules

[ramsay-t]

To produce Semantic Equivalence proofs in #6615 we will need some formalisations of notions of equivalence and some modules with useful lemmas etc.

• [ ] #7008
• [ ] #7048

[juloch1]

Can make this into a 4 nightly pull request so that the other team members can be able to have feedback on what is being done. This will bring down this ticket and split into sprints. @ramsay-t

[effectfully]

This is now inlined in #6611, so closing as duplicate.