Make equivalence work with receive

[jeltsch]

Currently, equivalence is not configured to perform rewriting under receive. The reason is that receive is not compatible with bisimilarity, but only quasi-compatible. However, by resolving input-output-hk/equivalence-reasoner#60, rewriting under receive becomes possible.

We shall configure the equivalence reasoner such that it performs rewriting also under receive. For that, we shall do the following:

• Add the following quasi-compatibility rule, with the compatibility attribute assigned to it, to the synchronous_transition_system locale:

  lemma receive_quasi_compatibility_rule [compatibility]:
    shows "A ▹ x. 𝒫 x ∼ A ▹ x. canonical (∼)⇧♯ 𝒫 x"

• Add the following compatibility-phase simplification rule:

  lemma receive_continuation_equivalence_class_lifting [compatibility_simplification]:
    shows "[𝒫]⇘K⇧♯⇙ = {𝒬. ∀n X. receive_follow_up 𝒬 n X ∈ [receive_follow_up 𝒫 n X]⇘K⇙}"

• Add an assignment of the compatibility_simplification attribute to the receive_follow_up_after lemmas