--- a/Paper/src/agda/_Fresh.agda.replaced	Thu Jan 12 20:31:09 2023 +0900
+++ b/Paper/src/agda/_Fresh.agda.replaced	Fri Jan 20 13:40:03 2023 +0900
@@ -1,7 +1,7 @@
 ------------------------------------------------------------------------
 -- The Agda standard library
 --
--- Fresh lists, a proof relevant variant of Catarina Coquand's contexts in
+-- Fresh lists, a proof relevant variant of Catarina Coquand!$\prime$!s contexts in
 -- "A Formalised Proof of the Soundness and Completeness of a Simply Typed
 -- Lambda-Calculus with Explicit Substitutions"
 ------------------------------------------------------------------------
@@ -15,8 +15,8 @@
 
 open import Level using (Level; _!$\sqcup$!_)
 open import Data.Bool.Base using (true; false)
-open import Data.Unit.Polymorphic.Base using (⊤)
-open import Data.Product using (∃; _!$\times$!_; _,_; -,_; proj!$\text{1}$!; proj₂)
+open import Data.Unit.Polymorphic.Base using (!$\top$!)
+open import Data.Product using (∃; _!$\times$!_; _,_; -,_; proj!$\text{1}$!; proj!$\text{2}$!)
 open import Data.List.Relation.Unary.All using (All; []; _!$\text{::}$!_)
 open import Data.List.Relation.Unary.AllPairs using (AllPairs; []; _!$\text{::}$!_)
 open import Data.Maybe.Base as Maybe using (Maybe; just; nothing)
@@ -57,7 +57,7 @@
   infixr 5 _!$\text{::}$!#_
   pattern _!$\text{::}$!#_ x xs = cons x xs _
 
-  fresh a []        = ⊤
+  fresh a []        = !$\top$!
   fresh a (x !$\text{::}$!# xs) = R a x !$\times$! fresh a xs
 
 -- Convenient notation for freshness making A and R implicit parameters
@@ -86,8 +86,8 @@
 
 module _ {R : Rel A r} {S : Rel A s} (R!$\Rightarrow$!S : ∀[ R !$\Rightarrow$! S ]) where
 
-  map₂ : List# A R !$\rightarrow$! List# A S
-  map₂ = map id R!$\Rightarrow$!S
+  map!$\text{2}$! : List# A R !$\rightarrow$! List# A S
+  map!$\text{2}$! = map id R!$\Rightarrow$!S
 
 ------------------------------------------------------------------------
 -- Views
@@ -136,7 +136,7 @@
 head = Maybe.map proj!$\text{1}$! ∘′ uncons
 
 tail : {R : Rel A r} !$\rightarrow$! List# A R !$\rightarrow$! Maybe (List# A R)
-tail = Maybe.map proj₂ ∘′ uncons
+tail = Maybe.map proj!$\text{2}$! ∘′ uncons
 
 take   : {R : Rel A r} !$\rightarrow$! !$\mathbb{N}$! !$\rightarrow$! List# A R !$\rightarrow$! List# A R
 take-# : {R : Rel A r} !$\rightarrow$! ∀ n a (as : List# A R) !$\rightarrow$! a # as !$\rightarrow$! a # take n as
@@ -195,7 +195,7 @@
 toAll  : ∀ {R : Rel A r} {a} as !$\rightarrow$! fresh A R a as !$\rightarrow$! All (R a) (proj!$\text{1}$! (toList as))
 
 toList []             = -, []
-toList (cons x xs ps) = -, toAll xs ps !$\text{::}$! proj₂ (toList xs)
+toList (cons x xs ps) = -, toAll xs ps !$\text{::}$! proj!$\text{2}$! (toList xs)
 
 toAll []        ps       = []
 toAll (a !$\text{::}$!# as) (p , ps) = p !$\text{::}$! toAll as ps