pragmatic note on matching against decidable equality

src/plfa/part2/Properties.lagda.md

@@ -775,6 +775,14 @@ Where the construct introduces a bound variable we need to compare it
 with the substituted variable, applying the drop lemma if they are
 equal and the swap lemma if they are distinct.
 
+Testing variable names for equality using the `_≟_` operator has a
+catch. For Agda it makes a difference whether we write `x ≟ y` or 
+`y ≟ x`. If the test matches the constraint that Agda expects, then the
+proof goes through as demonstrated. Otherwise, Agda produces a message
+that reveals the low-level implementation of string equality. To avoid
+this problem, the guideline is to always match literally on the expression
+on which Agda's evaluation is currently stuck.
+
 #### Exercise `subst′` (stretch)
 
 Rewrite `subst` to work with the modified definition `_[_:=_]′`