feat(#20): Replace □ with a dot-like Unicode symbol ⬝ for term application (Black Very Small Square, U+2B1D, \tr , \con)

.vscode/settings.json

@@ -13,8 +13,8 @@
     "~~": "~~",
     "~~e": "~~ₑ",
     "$n": "$ₙ",
-    "ap": "□",
-    "apn": "□ₙ",
+    "ap": "⬝",
+    "apn": "⬝ₙ",
     "d-": "↧",
     "d2": "￬",
     "Fun": "ƛ",

Plfl/DeBruijn.lean

@@ -84,7 +84,7 @@ namespace Term
   prefix:50 "μ " => mu
   notation "𝟘? " => case
   infixr:min " $ " => ap
-  infixl:70 " □ " => ap
+  infixl:70 " ⬝ " => ap
   prefix:80 "ι " => succ
   prefix:90 "‵" => var
   notation "𝟘" => zero
@@ -110,10 +110,10 @@ namespace Term
   example : Γ ⊢ ℕt := ι ι 𝟘
   example : Γ ⊢ ℕt := 2
 
-  @[simp] abbrev add : Γ ⊢ ℕt =⇒ ℕt =⇒ ℕt := μ ƛ ƛ (𝟘? (#1) (#0) (ι (#3 □ #0 □ #1)))
-  @[simp] abbrev mul : Γ ⊢ ℕt =⇒ ℕt =⇒ ℕt := μ ƛ ƛ (𝟘? (#1) 𝟘 (add □ #1 $ #3 □ #0 □ #1))
+  @[simp] abbrev add : Γ ⊢ ℕt =⇒ ℕt =⇒ ℕt := μ ƛ ƛ (𝟘? (#1) (#0) (ι (#3 ⬝ #0 ⬝ #1)))
+  @[simp] abbrev mul : Γ ⊢ ℕt =⇒ ℕt =⇒ ℕt := μ ƛ ƛ (𝟘? (#1) 𝟘 (add ⬝ #1 $ #3 ⬝ #0 ⬝ #1))
 
-  example : Γ ⊢ ℕt := add □ 2 □ 2
+  example : Γ ⊢ ℕt := add ⬝ 2 ⬝ 2
 
   /--
   The Church numeral Ty.
@@ -122,11 +122,11 @@ namespace Term
 
   @[simp] abbrev succC : Γ ⊢ ℕt =⇒ ℕt := ƛ ι #0
   @[simp] abbrev twoC : Γ ⊢ Ch a := ƛ ƛ (#1 $ #1 $ #0)
-  @[simp] abbrev addC : Γ ⊢ Ch a =⇒ Ch a =⇒ Ch a := ƛ ƛ ƛ ƛ (#3 □ #1 $ #2 □ #1 □ #0)
-  example : Γ ⊢ ℕt := addC □ twoC □ twoC □ succC □ 𝟘
+  @[simp] abbrev addC : Γ ⊢ Ch a =⇒ Ch a =⇒ Ch a := ƛ ƛ ƛ ƛ (#3 ⬝ #1 $ #2 ⬝ #1 ⬝ #0)
+  example : Γ ⊢ ℕt := addC ⬝ twoC ⬝ twoC ⬝ succC ⬝ 𝟘
 
   -- https://plfa.github.io/DeBruijn/#exercise-mul-recommended
-  @[simp] abbrev mulC : Γ ⊢ Ch a =⇒ Ch a =⇒ Ch a := ƛ ƛ ƛ ƛ (#3 □ (#2 □ #1) □ #0)
+  @[simp] abbrev mulC : Γ ⊢ Ch a =⇒ Ch a =⇒ Ch a := ƛ ƛ ƛ ƛ (#3 ⬝ (#2 ⬝ #1) ⬝ #0)
 end Term
 
 -- https://plfa.github.io/DeBruijn/#renaming
@@ -147,7 +147,7 @@ def rename : (∀ {a}, Γ ∋ a → Δ ∋ a) → Γ ⊢ a → Δ ⊢ a := by
   intro ρ; intro
   | ‵ x => exact ‵ (ρ x)
   | ƛ n => refine .lam ?_; refine rename ?_ n; exact ext ρ
-  | l □ m =>
+  | l ⬝ m =>
     apply Term.ap
     · exact rename ρ l
     · exact rename ρ m
@@ -186,7 +186,7 @@ def subst : (∀ {a}, Γ ∋ a → Δ ⊢ a) → Γ ⊢ a → Δ ⊢ a := by
   intro σ; intro
   | ‵ x => exact σ x
   | ƛ n => refine .lam ?_; refine subst ?_ n; exact exts σ
-  | l □ m =>
+  | l ⬝ m =>
     apply Term.ap
     · exact subst σ l
     · exact subst σ m
@@ -212,7 +212,7 @@ notation:90 n "⟦" m "⟧" => subst₁ m n
 example
 : let m : ∅ ⊢ ℕt =⇒ ℕt := ƛ (ι #0)
   let m' : ∅‚ ℕt =⇒ ℕt ⊢ ℕt =⇒ ℕt := ƛ (#1 $ #1 $ #0)
-  let n : ∅ ⊢ ℕt =⇒ ℕt := ƛ (ƛ ι #0) □ ((ƛ ι #0) □ #0)
+  let n : ∅ ⊢ ℕt =⇒ ℕt := ƛ (ƛ ι #0) ⬝ ((ƛ ι #0) ⬝ #0)
   m'⟦m⟧ = n
 := rfl
 
@@ -242,9 +242,9 @@ end Value
 `Reduce t t'` says that `t` reduces to `t'`.
 -/
 inductive Reduce : (Γ ⊢ a) → (Γ ⊢ a) → Type where
-| lamβ : Value w → Reduce ((ƛ n) □ w) (n⟦w⟧)
-| apξ₁ : Reduce l l' → Reduce (l □ m) (l' □ m)
-| apξ₂ : Value v → Reduce m m' → Reduce (v □ m) (v □ m')
+| lamβ : Value w → Reduce ((ƛ n) ⬝ w) (n⟦w⟧)
+| apξ₁ : Reduce l l' → Reduce (l ⬝ m) (l' ⬝ m)
+| apξ₂ : Value v → Reduce m m' → Reduce (v ⬝ m) (v ⬝ m')
 | zeroβ : Reduce (𝟘? 𝟘 m n) m
 | succβ : Value v → Reduce (𝟘? (ι v) m n) (n⟦v⟧)
 | succξ : Reduce m m' → Reduce (ι m) (ι m')
@@ -299,11 +299,11 @@ namespace Reduce
   open Term
 
   -- https://plfa.github.io/DeBruijn/#examples
-  example : twoC □ succC □ @zero ∅ —↠ 2 := calc
-    twoC □ succC □ 𝟘
-    _ —→ (ƛ (succC $ succC $ #0)) □ 𝟘 := by apply apξ₁; apply lamβ; exact Value.lam
+  example : twoC ⬝ succC ⬝ @zero ∅ —↠ 2 := calc
+    twoC ⬝ succC ⬝ 𝟘
+    _ —→ (ƛ (succC $ succC $ #0)) ⬝ 𝟘 := by apply apξ₁; apply lamβ; exact Value.lam
     _ —→ (succC $ succC $ 𝟘) := by apply lamβ; exact V𝟘
-    _ —→ succC □ 1 := by
+    _ —→ succC ⬝ 1 := by
       apply apξ₂
       · apply Value.lam
       · unfold succC; exact lamβ V𝟘
@@ -332,7 +332,7 @@ def progress : (m : ∅ ⊢ a) → Progress m := open Progress Reduce in by
   intro
   | ‵ _ => contradiction
   | ƛ _ => exact .done Value.lam
-  | jl □ jm => cases progress jl with
+  | jl ⬝ jm => cases progress jl with
     | step => apply step; · apply apξ₁; trivial
     | done vl => cases progress jm with
       | step => apply step; apply apξ₂ <;> trivial
@@ -382,12 +382,12 @@ info: DeBruijn.Result.dnf
 info: DeBruijn.Result.done
   (DeBruijn.Value.succ (DeBruijn.Value.succ (DeBruijn.Value.succ (DeBruijn.Value.succ (DeBruijn.Value.zero)))))
 -/
-#guard_msgs in #eval eval 100 (add □ 2 □ 2) |> (·.3)
+#guard_msgs in #eval eval 100 (add ⬝ 2 ⬝ 2) |> (·.3)
   /--
 info: DeBruijn.Result.done
   (DeBruijn.Value.succ
     (DeBruijn.Value.succ
       (DeBruijn.Value.succ (DeBruijn.Value.succ (DeBruijn.Value.succ (DeBruijn.Value.succ (DeBruijn.Value.zero)))))))
 -/
-#guard_msgs in #eval eval 100 (mul □ 2 □ 3) |> (·.3)
+#guard_msgs in #eval eval 100 (mul ⬝ 2 ⬝ 3) |> (·.3)
 end examples

Plfl/Lambda.lean

@@ -30,7 +30,7 @@ namespace Term
   notation:50 " μ " v " : " d => mu v d
   notation:max "𝟘? " e " [zero: " o " |succ " n " : " i " ] " => case e o n i
   infixr:min " $ " => ap
-  infixl:70 " □ " => ap
+  infixl:70 " ⬝ " => ap
   prefix:80 "ι " => succ
   prefix:90 "‵" => var
   notation "𝟘" => zero
@@ -45,17 +45,17 @@ namespace Term
   example : Term := 1
   example : Term := 42
 
-  abbrev add : Term := μ "+" : ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: ‵"n" |succ "m": ι (‵"+" □ ‵"m" □ ‵"n")]
+  abbrev add : Term := μ "+" : ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: ‵"n" |succ "m": ι (‵"+" ⬝ ‵"m" ⬝ ‵"n")]
   -- https://plfa.github.io/Lambda/#exercise-mul-recommended
-  abbrev mul : Term := μ "*" : ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: 𝟘 |succ "m": add □ ‵"n" $ ‵"*" □ ‵"m" □ ‵"n"]
+  abbrev mul : Term := μ "*" : ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: 𝟘 |succ "m": add ⬝ ‵"n" $ ‵"*" ⬝ ‵"m" ⬝ ‵"n"]
 
   -- Church encoding...
   abbrev succC : Term := ƛ "n" : ι ‵"n"
   abbrev oneC : Term := ƛ "s" : ƛ "z" : ‵"s" $ ‵"z"
   abbrev twoC : Term := ƛ "s" : ƛ "z" : ‵"s" $ ‵"s" $ ‵"z"
-  abbrev addC : Term := ƛ "m" : ƛ "n" : ƛ "s" : ƛ "z" : ‵"m" □ ‵"s" $ ‵"n" □ ‵"s" □ ‵"z"
+  abbrev addC : Term := ƛ "m" : ƛ "n" : ƛ "s" : ƛ "z" : ‵"m" ⬝ ‵"s" $ ‵"n" ⬝ ‵"s" ⬝ ‵"z"
   -- https://plfa.github.io/Lambda/#exercise-mul%E1%B6%9C-practice
-  abbrev mulC : Term := ƛ "m" : ƛ "n" : ƛ "s" : ƛ "z" : ‵"m" □ (‵"n" □ ‵"s") □ ‵"z"
+  abbrev mulC : Term := ƛ "m" : ƛ "n" : ƛ "s" : ƛ "z" : ‵"m" ⬝ (‵"n" ⬝ ‵"s") ⬝ ‵"z"
 end Term
 
 -- https://plfa.github.io/Lambda/#values
@@ -96,10 +96,10 @@ namespace Term
 
   -- https://plfa.github.io/Lambda/#examples
   example
-  : (ƛ "z" : ‵"s" □ ‵"s" □ ‵"z")["s" := succC]
-  = (ƛ "z" : succC □ succC □ ‵"z") := rfl
+  : (ƛ "z" : ‵"s" ⬝ ‵"s" ⬝ ‵"z")["s" := succC]
+  = (ƛ "z" : succC ⬝ succC ⬝ ‵"z") := rfl
 
-  example : (succC □ succC □ ‵"z")["z" := 𝟘] = succC □ succC □ 𝟘 := rfl
+  example : (succC ⬝ succC ⬝ ‵"z")["z" := 𝟘] = succC ⬝ succC ⬝ 𝟘 := rfl
   example : (ƛ "x" : ‵"y")["y" := 𝟘] = (ƛ "x" : 𝟘) := rfl
   example : (ƛ "x" : ‵"x")["x" := 𝟘] = (ƛ "x" : ‵"x") := rfl
   example : (ƛ "y" : ‵"y")["x" := 𝟘] = (ƛ "y" : ‵"y") := rfl
@@ -115,9 +115,9 @@ namespace Term
   `Reduce t t'` says that `t` reduces to `t'`.
   -/
   inductive Reduce : Term → Term → Type where
-  | lamβ : Value v → Reduce ((ƛ x : n) □ v) (n[x := v])
-  | apξ₁ : Reduce l l' → Reduce (l □ m) (l' □ m)
-  | apξ₂ : Value v → Reduce m m' → Reduce (v □ m) (v □ m')
+  | lamβ : Value v → Reduce ((ƛ x : n) ⬝ v) (n[x := v])
+  | apξ₁ : Reduce l l' → Reduce (l ⬝ m) (l' ⬝ m)
+  | apξ₂ : Value v → Reduce m m' → Reduce (v ⬝ m) (v ⬝ m')
   | zeroβ : Reduce (𝟘? 𝟘 [zero: m |succ x : n]) m
   | succβ : Value v → Reduce (𝟘? ι v [zero: m |succ x : n]) (n[x := v])
   | succξ : Reduce m m' → Reduce (ι m) (ι m')
@@ -130,13 +130,13 @@ end Term
 
 namespace Term.Reduce
   -- https://plfa.github.io/Lambda/#quiz-1
-  example : (ƛ "x" : ‵"x") □ (ƛ "x" : ‵"x") —→ (ƛ "x" : ‵"x") := by
+  example : (ƛ "x" : ‵"x") ⬝ (ƛ "x" : ‵"x") —→ (ƛ "x" : ‵"x") := by
     apply lamβ; exact Value.lam
 
-  example : (ƛ "x" : ‵"x") □ (ƛ "x" : ‵"x") □ (ƛ "x" : ‵"x") —→ (ƛ "x" : ‵"x") □ (ƛ "x" : ‵"x") := by
+  example : (ƛ "x" : ‵"x") ⬝ (ƛ "x" : ‵"x") ⬝ (ƛ "x" : ‵"x") —→ (ƛ "x" : ‵"x") ⬝ (ƛ "x" : ‵"x") := by
     apply apξ₁; apply lamβ; exact Value.lam
 
-  example : twoC □ succC □ 𝟘 —→ (ƛ "z" : succC $ succC $ ‵"z") □ 𝟘 := by
+  example : twoC ⬝ succC ⬝ 𝟘 —→ (ƛ "z" : succC $ succC $ ‵"z") ⬝ 𝟘 := by
     unfold twoC; apply apξ₁; apply lamβ; exact Value.lam
 
   -- https://plfa.github.io/Lambda/#reflexive-and-transitive-closure
@@ -246,29 +246,29 @@ end confluence
 section examples
   open Term Term.Reduce Term.Reduce.Clos
 
-  example : twoC □ succC □ 𝟘 —↠ 2 := calc
-    twoC □ succC □ 𝟘
-    _ —→ (ƛ "z" : succC $ succC $ ‵"z") □ 𝟘 := by apply apξ₁; apply lamβ; exact Value.lam
+  example : twoC ⬝ succC ⬝ 𝟘 —↠ 2 := calc
+    twoC ⬝ succC ⬝ 𝟘
+    _ —→ (ƛ "z" : succC $ succC $ ‵"z") ⬝ 𝟘 := by apply apξ₁; apply lamβ; exact Value.lam
     _ —→ (succC $ succC $ 𝟘) := by apply lamβ; exact Value.zero
-    _ —→ succC □ 1 := by apply apξ₂; apply Value.lam; apply lamβ; exact Value.zero
+    _ —→ succC ⬝ 1 := by apply apξ₂; apply Value.lam; apply lamβ; exact Value.zero
     _ —→ 2 := by apply lamβ; exact Value.ofNat 1
 
   -- https://plfa.github.io/Lambda/#exercise-plus-example-practice
-  example : add □ 1 □ 1 —↠ 2 := calc
-    add □ 1 □ 1
-    _ —→ (ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: ‵"n" |succ "m": ι (add □ ‵"m" □ ‵"n")]) □ 1 □ 1
+  example : add ⬝ 1 ⬝ 1 —↠ 2 := calc
+    add ⬝ 1 ⬝ 1
+    _ —→ (ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: ‵"n" |succ "m": ι (add ⬝ ‵"m" ⬝ ‵"n")]) ⬝ 1 ⬝ 1
       := by apply apξ₁; apply apξ₁; apply muβ
-    _ —↠ (ƛ "n" : 𝟘? 1 [zero: ‵"n" |succ "m": ι (add □ ‵"m" □ ‵"n")]) □ 1
+    _ —↠ (ƛ "n" : 𝟘? 1 [zero: ‵"n" |succ "m": ι (add ⬝ ‵"m" ⬝ ‵"n")]) ⬝ 1
       := .one <| by apply apξ₁; apply lamβ; exact Value.ofNat 1
-    _ —→ 𝟘? 1 [zero: 1 |succ "m": ι (add □ ‵"m" □ 1)]
+    _ —→ 𝟘? 1 [zero: 1 |succ "m": ι (add ⬝ ‵"m" ⬝ 1)]
       := lamβ <| Value.ofNat 1
-    _ —→ ι (add □ 𝟘 □ 1)
+    _ —→ ι (add ⬝ 𝟘 ⬝ 1)
       := succβ Value.zero
-    _ —→ ι ((ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: ‵"n" |succ "m": ι (add □ ‵"m" □ ‵"n")]) □ 𝟘 □ 1)
+    _ —→ ι ((ƛ "m" : ƛ "n" : 𝟘? ‵"m" [zero: ‵"n" |succ "m": ι (add ⬝ ‵"m" ⬝ ‵"n")]) ⬝ 𝟘 ⬝ 1)
       := by apply succξ; apply apξ₁; apply apξ₁; apply muβ
-    _ —→ ι ((ƛ "n" : 𝟘? 𝟘 [zero: ‵"n" |succ "m": ι (add □ ‵"m" □ ‵"n")]) □ 1)
+    _ —→ ι ((ƛ "n" : 𝟘? 𝟘 [zero: ‵"n" |succ "m": ι (add ⬝ ‵"m" ⬝ ‵"n")]) ⬝ 1)
       := by apply succξ; apply apξ₁; apply lamβ; exact V𝟘
-    _ —→ ι (𝟘? 𝟘 [zero: 1 |succ "m": ι (add □ ‵"m" □ 1)])
+    _ —→ ι (𝟘? 𝟘 [zero: 1 |succ "m": ι (add ⬝ ‵"m" ⬝ 1)])
       := by apply succξ; apply lamβ; exact Value.ofNat 1
     _ —→ 2 := succξ zeroβ
 end examples
@@ -343,7 +343,7 @@ namespace Context
   inductive IsTy : Context → Term → Ty → Type where
   | tyVar : Γ ∋ x ⦂ t → IsTy Γ (‵x) t
   | tyLam : IsTy (Γ‚ x ⦂ t) n u → IsTy Γ (ƛ x : n) (t =⇒ u)
-  | tyAp : IsTy Γ l (t =⇒ u) → IsTy Γ x t → IsTy Γ (l □ x) u
+  | tyAp : IsTy Γ l (t =⇒ u) → IsTy Γ x t → IsTy Γ (l ⬝ x) u
   | tyZero : IsTy Γ 𝟘 ℕt
   | tySucc : IsTy Γ n ℕt → IsTy Γ (ι n) ℕt
   | tyCase : IsTy Γ l ℕt → IsTy Γ m t → IsTy (Γ‚ x ⦂ ℕt) n t → IsTy Γ (𝟘? l [zero: m |succ x: n]) t
@@ -383,7 +383,7 @@ namespace Context
       · trivial
       · exact tyZero
 
-  def two_ty : Γ ⊢ (ƛ "s" : ‵"s" $ ‵"s" $ 𝟘) □ succC ⦂ ℕt := by
+  def two_ty : Γ ⊢ (ƛ "s" : ‵"s" $ ‵"s" $ 𝟘) ⬝ succC ⦂ ℕt := by
     apply tyAp twice_ty
     · apply tyLam; apply tySucc; trivial
 
@@ -416,25 +416,25 @@ section examples
   open Term Context Lookup Context.IsTy
 
   -- https://plfa.github.io/Lambda/#non-examples
-  example : ∅ ⊬ 𝟘 □ 1 :=
+  example : ∅ ⊬ 𝟘 ⬝ 1 :=
     ⟨fun | .tyAp hl _ => by cases hl⟩
 
-  abbrev illLam := ƛ "x" : ‵"x" □ ‵"x"
+  abbrev illLam := ƛ "x" : ‵"x" ⬝ ‵"x"
 
   lemma nty_illLam : ∅ ⊬ illLam :=
     ⟨fun | .tyLam (.tyAp (.tyVar hx) (.tyVar hx')) => Ty.t_to_t'_ne_t _ _ (Lookup.functional hx hx')⟩
 
   -- https://plfa.github.io/Lambda/#quiz-3
-  example : ∅‚ "y" ⦂ ℕt =⇒ ℕt‚ "x" ⦂ ℕt ⊢ ‵"y" □ ‵"x" ⦂ ℕt := by
+  example : ∅‚ "y" ⦂ ℕt =⇒ ℕt‚ "x" ⦂ ℕt ⊢ ‵"y" ⬝ ‵"x" ⦂ ℕt := by
     apply tyAp <;> trivial
 
-  example : ∅‚ "y" ⦂ ℕt =⇒ ℕt‚ "x" ⦂ ℕt ⊬ ‵"x" □ ‵"y" :=
+  example : ∅‚ "y" ⦂ ℕt =⇒ ℕt‚ "x" ⦂ ℕt ⊬ ‵"x" ⬝ ‵"y" :=
     ⟨fun | .tyAp (.tyVar hx) _ => by cases hx with | s _ _ => contradiction⟩
 
-  example : ∅‚ "y" ⦂ ℕt =⇒ ℕt ⊢ ƛ "x" : ‵"y" □ ‵"x" ⦂ ℕt =⇒ ℕt := by
+  example : ∅‚ "y" ⦂ ℕt =⇒ ℕt ⊢ ƛ "x" : ‵"y" ⬝ ‵"x" ⦂ ℕt =⇒ ℕt := by
     apply tyLam; apply tyAp <;> trivial
 
-  example : ∅‚ "x" ⦂ t ⊬ ‵"x" □ ‵"x" :=
+  example : ∅‚ "x" ⦂ t ⊬ ‵"x" ⬝ ‵"x" :=
     ⟨fun
     | .tyAp (.tyVar .z) (.tyVar (.s _ _)) => by contradiction
     | .tyAp (.tyVar (.s _ _)) _ => by contradiction⟩

Plfl/Lambda/Properties.lean

@@ -328,7 +328,7 @@ section examples
   -/
   #guard_msgs in #eval eval 3 tySuccμ |>.3
 
-  abbrev add_2_2 := add □ 2 □ 2
+  abbrev add_2_2 := add ⬝ 2 ⬝ 2
 
   abbrev two_ty : ∅ ⊢ 2 ⦂ ℕt := by
     iterate 2 (apply tySucc)
@@ -372,7 +372,7 @@ section subject_expansion
 example : IsEmpty (∀ {n t m}, ∅ ⊢ n ⦂ t → (m —→ n) → ∅ ⊢ m ⦂ t) := by
     by_contra f
     simp_all only [isEmpty_pi, not_exists, not_isEmpty_iff]
-    let illAp := (ƛ "x" : 𝟘) □ illLam
+    let illAp := (ƛ "x" : 𝟘) ⬝ illLam
     have nty_ill : ∅ ⊬ illAp := by
       intro tt
       refine ⟨fun j => ?_⟩
@@ -462,8 +462,8 @@ Which of the following properties remain true in the presence of these rules? Fo
 * Determinism
 
 Becomes false.
-The term `(ƛ x ⇒ `"x") □ 𝟘` can both be reduced via:
-· apξ₁, to zap □ 𝟘
+The term `(ƛ x ⇒ `"x") ⬝ 𝟘` can both be reduced via:
+· apξ₁, to zap ⬝ 𝟘
 · zepβ, to zap
 ... and they're not equal.
 
@@ -488,17 +488,17 @@ Which of the following properties remain true in the presence of this rule? For
 
 Becomes false.
 
-The term `(ƛ x ⇒ `"x") □ 𝟘` can both be reduced via:
-· apξ₁, to foo □ 𝟘
+The term `(ƛ x ⇒ `"x") ⬝ 𝟘` can both be reduced via:
+· apξ₁, to foo ⬝ 𝟘
 · lamβ, to `"x"
 ... and they're not equal.
 
 * Progress
 
 Becomes false.
-The term `(ƛ x ⇒ `"x") □ 𝟘` can be reduced via:
-· apξ₁ fooβ₁, to foo □ 𝟘
-· then apξ₁ fooβ₂, to 𝟘 □ 𝟘
+The term `(ƛ x ⇒ `"x") ⬝ 𝟘` can be reduced via:
+· apξ₁ fooβ₁, to foo ⬝ 𝟘
+· then apξ₁ fooβ₂, to 𝟘 ⬝ 𝟘
 ... and now the term get's stuck.
 
 * Preservation
@@ -522,7 +522,7 @@ Remains true.
 * Progress
 
 Becomes false.
-The term `(ƛ x ⇒ `"x") □ 𝟘` is well-typed but gets stucked.
+The term `(ƛ x ⇒ `"x") ⬝ 𝟘` is well-typed but gets stucked.
 -/
 
 -- https://plfa.github.io/Properties/#quiz-3