Who knows, please, why ``$`` is not type-checked when inserted into terms in the left column of the equality reasoning chain? For example, ``` begin f $ g x ≈⟨ proof ⟩ x ∎ ``` Probably this concerns the relation between the precedence of ``$`` and the precedence of the reasoning combinators. Thanks, ------ Sergei