--- a/Paper/src/agda-term2.agda.replaced	Sat Nov 06 20:06:24 2021 +0900
+++ b/Paper/src/agda-term2.agda.replaced	Sun Nov 07 00:51:16 2021 +0900
@@ -1,11 +1,11 @@
-+-comm : (x y : @$\mathbb{N}$@) @$\rightarrow$@ x + y @$\equiv$@ y + x
++-comm : (x y : !$\mathbb{N}$!) !$\rightarrow$! x + y !$\equiv$! y + x
 +-comm zero y rewrite (+zero {y}) = refl
-+-comm (suc x) y = let open @$\equiv$@-Reasoning in
++-comm (suc x) y = let open !$\equiv$!-Reasoning in
   begin
-  (suc x) + y @$\equiv$@@$\langle$@@$\rangle$@
-  suc (x + y) @$\equiv$@@$\langle$@ cong suc (+-comm x y) @$\rangle$@
-  suc (y + x) @$\equiv$@@$\langle$@ ?0 @$\rangle$@
-  ?1 @$\blacksquare$@
+  (suc x) + y !$\equiv$!!$\langle$!!$\rangle$!
+  suc (x + y) !$\equiv$!!$\langle$! cong suc (+-comm x y) !$\rangle$!
+  suc (y + x) !$\equiv$!!$\langle$! ?0 !$\rangle$!
+  ?1 !$\blacksquare$!
 
--- ?0 : suc (y + x) @$\equiv$@ y + suc x
+-- ?0 : suc (y + x) !$\equiv$! y + suc x
 -- ?1 : y + suc x