Improved text on difference from paper

papers/LMCS.md

@@ -27,8 +27,9 @@ in [papers/POPL20.md](POPL20.md), that are briefly discussed here.
 
 The paper presents a set of rules for the subprotocol relation with binders,
 namely `⊑-send-mono'`, `⊑-recv-mono'`, and `⊑-swap'`. These are not available
-in the mechanisation, for technical reasons related to the encoding of binders.
-However, the rules are admissible from the primitive rules, as explained in the
-paper. The consequence of this is observed in the proof of the Löb recursion
-example, which differs from the proof presented in the paper, as it uses the
-rules with binders.
+in the mechanisation, as applying them can be cumbersome, due to the encoding of
+the binders. However, the rules are admissible from the primitive rules, as
+explained in the paper. Additionally, working with the tactics, as elaborated on
+in the mechanisation section of the paper, is recommended. This can be observed in
+the proof of the Löb recursion example, which differs from the proof presented in
+the paper.