Properties: rename a proof for z ≢ x

2020-01-06 22:46:44 +01:00 · 2020-01-06 22:46:44 +01:00 · 338b959f95
commit 338b959f95
parent 6842ac170b
1 changed files with 1 additions and 1 deletions
--- a/src/plfa/part2/Properties.lagda.md
+++ b/src/plfa/part2/Properties.lagda.md
@ -568,7 +568,7 @@ swap {Γ} {x} {y} {M} {A} {B} {C} x≢y ⊢M = rename ρ ⊢M
      --------------------------
    → Γ , x ⦂ A , y ⦂ B ∋ z ⦂ C
  ρ Z                   =  S x≢y Z
-  ρ (S y≢x Z)           =  Z
+  ρ (S z≢x Z)           =  Z
  ρ (S z≢x (S z≢y ∋z))  =  S z≢y (S z≢x ∋z)
 ```
 Here the renaming map takes a variable at the end into a variable one