--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Paper/src/agda-term1.agda.replaced	Sun Apr 24 23:13:44 2022 +0900
@@ -0,0 +1,10 @@
++-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
+  begin
+  ?0 !$\equiv$!!$\langle$! ?1 !$\rangle$!
+  ?2 !$\blacksquare$!
+
+-- ?0 : !$\mathbb{N}$! {(suc x) + y}
+-- ?1 : suc x + y !$\equiv$! y + suc x
+-- ?2 : !$\mathbb{N}$!