--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/agda-term1.agda.replaced	Thu Feb 06 19:24:32 2020 +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}$@