Simplify Relation.Binary.Reasoning.Syntax further

[MatthewDaggitt]

I know I'm opening an issue for a yet non-existent module, but I don't want to forget this. If agda/agda#6918 was resolved then we could simplify this file further, e.g. by:

module _
  (_R_ : Rel A ℓ₁)
  {_S_ : Rel A ℓ₂}
  (sym : Symmetric _S_)
  (forward : Trans _S_ _R_ _R_)
  where
  
  infixr 2 forward-step backward-step

  -- Step with the setoid equality
  forward-step : ∀ (x : A) {y z} → y R z → x S y → x R z
  forward-step x yRz x≈y = forward {x} x≈y yRz

  -- Flipped step with the setoid equality
  backward-step : ∀ x {y z} → y R z → y S x → x R z
  backward-step x yRz x≈y = forward-step x yRz (sym x≈y)

  -- Setoid equality syntax
  module ≈-syntax where
    syntax forward-step  x yRz x≈y = x ≈⟨ x≈y ⟩ yRz
    syntax backward-step x yRz y≈x = x ≈˘⟨ y≈x ⟩ yRz

  -- Apartness relation syntax
  module #-syntax where
    syntax forward-step  x yRz x#y = x #⟨ x#y ⟩ yRz
    syntax backward-step x yRz y#x = x #˘⟨ y#x ⟩ yRz