Unnecessary axioms, bisimulations, renaming equivalence in the concurrent setup and Coq 8.18

[berpeti]

This pull request introduces the following improvements:

• Removes dependency on proof_irrelevance and propositional_extensionality axioms in the sequential semantics.
• Ports the project to work with Coq 8.18.
• Introduces finite map-based semantics for the concurrent sublanguage
• Proves a number of theorems about the properties of the concurrent semantics.
• Defines a number of bisimulation definitions to reason about program equivalence.
• Proves that renaming process identifiers results in equivalent concurrent programs (although, the proof is unguarded due to a use of symmetry of bisimulations).
• Introduces a number of work-in-progress, experimental developments.