diff --git a/src/plfa/part2/BigStep.lagda.md b/src/plfa/part2/BigStep.lagda.md
index f438d258..814e1f06 100644
--- a/src/plfa/part2/BigStep.lagda.md
+++ b/src/plfa/part2/BigStep.lagda.md
@@ -172,7 +172,7 @@ the environment `γ` to an equivalent substitution `σ`.
 The case for `⇓-app` also requires that we strengthen the
 conclusion. In the case for `⇓-app` we have `γ ⊢ L ⇓ clos (λ N) δ` and
 the induction hypothesis gives us `L —↠ ƛ N′`, but we need to know
-that `N` and `N′` are equivalent. In particular, that `N ≡ subst τ N′`
+that `N` and `N′` are equivalent. In particular, that `N′ ≡ subst τ N`
 where `τ` is the substitution that is equivalent to `δ`. Therefore we
 expand the conclusion of the statement, stating that the results are
 equivalent.
@@ -279,22 +279,22 @@ to some term `N` that is equivalent to `V`. We describe the proof
 below.
 
 ```
-⇓→—↠×𝔹 : ∀{Γ}{γ : ClosEnv Γ}{σ : Subst Γ ∅}{M : Γ ⊢ ★}{V : Clos}
+⇓→—↠×≈ : ∀{Γ}{γ : ClosEnv Γ}{σ : Subst Γ ∅}{M : Γ ⊢ ★}{V : Clos}
        → γ ⊢ M ⇓ V  →  γ ≈ₑ σ
          ---------------------------------------
        → Σ[ N ∈ ∅ ⊢ ★ ] (subst σ M —↠ N) × V ≈ N
-⇓→—↠×𝔹 {γ = γ} (⇓-var{x = x} γx≡Lδ δ⊢L⇓V) γ≈ₑσ
+⇓→—↠×≈ {γ = γ} (⇓-var{x = x} γx≡Lδ δ⊢L⇓V) γ≈ₑσ
     with γ x | γ≈ₑσ {x} | γx≡Lδ
 ... | clos L δ | ⟨ τ , ⟨ δ≈ₑτ , σx≡τL ⟩ ⟩ | refl
-      with ⇓→—↠×𝔹{σ = τ} δ⊢L⇓V δ≈ₑτ
+      with ⇓→—↠×≈{σ = τ} δ⊢L⇓V δ≈ₑτ
 ...   | ⟨ N , ⟨ τL—↠N , V≈N ⟩ ⟩ rewrite σx≡τL =
         ⟨ N , ⟨ τL—↠N , V≈N ⟩ ⟩
-⇓→—↠×𝔹 {σ = σ} {V = clos (ƛ N) γ} ⇓-lam γ≈ₑσ =
+⇓→—↠×≈ {σ = σ} {V = clos (ƛ N) γ} (⇓-lam) γ≈ₑσ =
     ⟨ subst σ (ƛ N) , ⟨ subst σ (ƛ N) ∎ , ⟨ σ , ⟨ γ≈ₑσ , refl ⟩ ⟩ ⟩ ⟩
-⇓→—↠×𝔹{Γ}{γ} {σ = σ} {L · M} {V} (⇓-app {N = N} L⇓ƛNδ N⇓V) γ≈ₑσ
-    with ⇓→—↠×𝔹{σ = σ} L⇓ƛNδ γ≈ₑσ
-... | ⟨ _ , ⟨ σL—↠ƛτN , ⟨ τ , ⟨ δ≈ₑτ , ≡ƛτN ⟩ ⟩ ⟩ ⟩ rewrite ≡ƛτN
-      with ⇓→—↠×𝔹 {σ = ext-subst τ (subst σ M)} N⇓V
+⇓→—↠×≈{Γ}{γ} {σ = σ} {L · M} {V} (⇓-app {N = N} L⇓ƛNδ N⇓V) γ≈ₑσ
+    with ⇓→—↠×≈{σ = σ} L⇓ƛNδ γ≈ₑσ
+... | ⟨ _ , ⟨ σL—↠ƛτN , ⟨ τ , ⟨ δ≈ₑτ , ≡ƛτN ⟩ ⟩ ⟩ ⟩ rewrite ≡ƛτN 
+      with ⇓→—↠×≈ {σ = ext-subst τ (subst σ M)} N⇓V
              (λ {x} → ≈ₑ-ext{σ = τ} δ≈ₑτ ⟨ σ , ⟨ γ≈ₑσ , refl ⟩ ⟩ {x})
            | β{∅}{subst (exts τ) N}{subst σ M}
 ...   | ⟨ N' , ⟨ —↠N' , V≈N' ⟩ ⟩ | ƛτN·σM—→
@@ -367,7 +367,7 @@ cbn→reduce :  ∀{M : ∅ ⊢ ★}{Δ}{δ : ClosEnv Δ}{N′ : Δ , ★ ⊢ 
     -----------------------------
   → Σ[ N ∈ ∅ , ★ ⊢ ★ ] (M —↠ ƛ N)
 cbn→reduce {M}{Δ}{δ}{N′} M⇓c
-    with ⇓→—↠×𝔹{σ = ids} M⇓c ≈ₑ-id
+    with ⇓→—↠×≈{σ = ids} M⇓c ≈ₑ-id
 ... | ⟨ N , ⟨ rs , ⟨ σ , ⟨ h , eq2 ⟩ ⟩ ⟩ ⟩ rewrite sub-id{M = M} | eq2 =
       ⟨ subst (exts σ) N′ , rs ⟩
 ```
diff --git a/src/plfa/part2/Confluence.lagda.md b/src/plfa/part2/Confluence.lagda.md
index 17faee5a..48651bc9 100644
--- a/src/plfa/part2/Confluence.lagda.md
+++ b/src/plfa/part2/Confluence.lagda.md
@@ -67,7 +67,7 @@ open import Data.Product using (_×_; Σ; Σ-syntax; ∃; ∃-syntax; proj₁; p
   renaming (_,_ to ⟨_,_⟩)
 open import plfa.part2.Substitution using (Rename; Subst)
 open import plfa.part2.Untyped
-  using (_—→_; β; ξ₁; ξ₂; ζ; _—↠_; _—→⟨_⟩_; _∎;
+  using (_—→_; β; ξ₁; ξ₂; ζ; _—↠_; begin_; _—→⟨_⟩_; _—↠⟨_⟩_; _∎;
   abs-cong; appL-cong; appR-cong; —↠-trans;
   _⊢_; _∋_; `_; #_; _,_; ★; ƛ_; _·_; _[_];
   rename; ext; exts; Z; S_; subst; subst-zero)
@@ -195,17 +195,19 @@ par-betas : ∀{Γ A}{M N : Γ ⊢ A}
   → M —↠ N
 par-betas {Γ} {A} {.(` _)} (pvar{x = x}) = (` x) ∎
 par-betas {Γ} {★} {ƛ N} (pabs p) = abs-cong (par-betas p)
-par-betas {Γ} {★} {L · M} (papp p₁ p₂) =
-   —↠-trans (appL-cong{M = M} (par-betas p₁)) (appR-cong (par-betas p₂))
+par-betas {Γ} {★} {L · M} (papp {L = L}{L′}{M}{M′} p₁ p₂) =
+    begin
+    L · M   —↠⟨ appL-cong{M = M} (par-betas p₁) ⟩
+    L′ · M  —↠⟨ appR-cong (par-betas p₂) ⟩
+    L′ · M′
+    ∎
 par-betas {Γ} {★} {(ƛ N) · M} (pbeta{N′ = N′}{M′ = M′} p₁ p₂) =
-  let ih₁ = par-betas p₁ in
-  let ih₂ = par-betas p₂ in
-  let a : (ƛ N) · M —↠ (ƛ N′) · M
-      a = appL-cong{M = M} (abs-cong ih₁) in
-  let b : (ƛ N′) · M —↠ (ƛ N′) · M′
-      b = appR-cong{L = ƛ N′} ih₂ in
-  let c = (ƛ N′) · M′ —→⟨ β ⟩ N′ [ M′ ] ∎ in
-  —↠-trans (—↠-trans a b) c
+    begin
+    (ƛ N) · M                    —↠⟨ appL-cong{M = M} (abs-cong (par-betas p₁)) ⟩
+    (ƛ N′) · M                   —↠⟨ appR-cong{L = ƛ N′} (par-betas p₂)  ⟩
+    (ƛ N′) · M′                  —→⟨ β ⟩
+     N′ [ M′ ]
+    ∎
 ```
 
 The proof is by induction on `M ⇛ N`.
@@ -219,14 +221,13 @@ The proof is by induction on `M ⇛ N`.
 * Suppose `L · M ⇛ L′ · M′` because `L ⇛ L′` and `M ⇛ M′`.
   By the induction hypothesis, we have `L —↠ L′` and `M —↠ M′`.
   So `L · M —↠ L′ · M` and then `L′ · M  —↠ L′ · M′`
-  because `—↠` is a congruence. We conclude using the transitity
-  of `—↠`.
+  because `—↠` is a congruence. 
 
 * Suppose `(ƛ N) · M  ⇛  N′ [ M′ ]` because `N ⇛ N′` and `M ⇛ M′`.
   By similar reasoning, we have
-  `(ƛ N) · M —↠ (ƛ N′) · M′`.
-  Of course, `(ƛ N′) · M′ —→ N′ [ M′ ]`, so we can conclude
-  using the transitivity of `—↠`.
+  `(ƛ N) · M —↠ (ƛ N′) · M′`
+  which we can following with the β reduction
+  `(ƛ N′) · M′ —→ N′ [ M′ ]`.
 
 With this lemma in hand, we complete the proof that `M ⇛* N` implies
 `M —↠ N` with a simple induction on `M ⇛* N`.