From c86266a4c4339a4fada479f5ce968bcd5c3ab43c Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Wed, 28 Oct 2020 13:39:43 +0100
Subject: [PATCH] Improved text on difference from paper

---
 papers/LMCS.md | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/papers/LMCS.md b/papers/LMCS.md
index e217303..81e9f3b 100644
--- a/papers/LMCS.md
+++ b/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.
-- 
GitLab