Merge pull request plfa#356 from mdimjasevic/prop-subst-var

Properties: fixes a typing judgment by replacing an identifier with a term

Author: wadler

src/plfa/Properties.lagda.md

@@ -656,8 +656,8 @@ Now that naming is resolved, let's unpack the first three cases:
 
   + The lookup judgment is evidenced by rule `Z`:
 
-        -----------------
-        Γ , x ⦂ A ⊢ x ⦂ A
+        ----------------
+        Γ , x ⦂ A ∋ x ⦂ A
 
     In this case, `x` and `y` are necessarily identical, as are `A`
     and `B`.  Nonetheless, we must evaluate `x ≟ y` in order to allow