Reasoning syntax doesn't produce the expected result for relations which aren't strictly left unital

[VojtechStep]

Equational reasoning works as advertised: equational-reasoning x ＝ y by p computes to p, but it relies on refl being a strict left unit with respect to path composition, since the syntax expands to refl ∙ p.

This doesn't work anymore for e.g. equivalence reasoning, where equivalence-reasoning X ≃ Y by e computes to e ∘e id-equiv, not e as claimed.

The way this reasoning syntax currently works is that there's an X-reasoning_ operator which binds strongly and creates the left unit, and then the steps apply transitivity. I believe it can be reimplemented so that the steps bind strongly, and then X-reasoning_ would be the identity, but that's just speculation at this point.