Add `family_uncurry_after_` lemmas for the communication primitives

[javierdiaz72]

Currently, we have family_uncurry_after_ lemmas for the constructs of the Þ-calculus. We shall extend this configuration to include family_uncurry_after_ lemmas also for the communication language primitives. In addition, we shall add these new lemmas to the built-in list of pre-simplification rules.

[jeltsch]

Could you maybe resolve this right now as part of #23? When resolving it, please take care to not introduce an extra lemmas specification for assigning the induct_simp attribute, but assign induct_simp within the lemmas themselves. In the Þ-calculus, it makes sense to have that separate lemmas specification, since making the lemmas in question pre-simplification rules can only be motivated once we have the synchronous transition system defined, while the lemmas themselves appear already in Thorn_Calculus-Foundations and Thorn_Calculus-Processes.

[javierdiaz72]

Could you maybe resolve this right now as part of #23?

Please note that pushing these changes as part of #23 would make the automated builds fail since we should first merge input-output-hk/thorn-calculus#76 into master. Should I go ahead nevertheless?