feat(Relation): add TransGenCommute, SemiDiamondCommute

[lengyijun]

Introduce intermediate commutation notions between single-step and multi-step properties:

• TransGenCommute: single r₁ + single r₂ join via TransGen r₂ and ReflTransGen r₁
• SemiDiamondCommute: single r₁ + TransGen r₂ join via TransGen r₂ and ReflTransGen r₁

Prove the corresponding implications and equivalences mirroring the existing SemiCommute ↔ Commute development, including:

• SemiDiamondCommute ↔ DiamondCommute (ReflTransGen r₁) (TransGen r₂)
• Commute ∧ TransGenCommute ↔ SemiDiamondCommute

[lengyijun]

Part 1 of #965: postpone-related relations.

@thomaskwaring @SamuelSchlesinger could you please take a look and review this?

[thomaskwaring]

Thanks! sorry I haven't had the chance to review your other PR yet.

I'll look properly this soon, but I would like if possible a bit of motivation — we now have a whole sea of different commutation & confluence properties so it would be nice to know what each of them is for. Am I right in thinking the important difference between these definitions and the ones we have is that it enforces a positive number of steps for one of the relations? (I vaguely remember that being important for some sort of standardisation argument.)

[lengyijun]

The main motivation is to prove

theorem sn_eta_steps_iff [DecidableEq Var] [HasFresh Var] (steps : t ↠ηᶠ t') :
    SN FullBeta t ↔ SN FullBeta t'

This requires the following postponement result:

diamondcommute_etaplus_betastar:
  if P ↠ηᶠ Q and Q ↠β+ R, then there exists a term S such that
  P ↠β+ S and S ↠ηᶠ R.

[lengyijun]

Am I right in thinking the important difference between these definitions and the ones we have is that it enforces a positive number of steps for one of the relations? (I vaguely remember that being important for some sort of standardisation argument.)

Exactly

SN (TransGen r) = SN r