--- a/paper/src/AgdaLambda.agda.replaced	Wed Feb 05 02:48:31 2020 +0900
+++ b/paper/src/AgdaLambda.agda.replaced	Thu Feb 06 19:24:32 2020 +0900
@@ -1,5 +1,5 @@
-not-apply : Bool @$\rightarrow$@ Bool
-not-apply = (\b @$\rightarrow$@ not b)   -- use lambda
++1 : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@
++1 n = suc n -- not use lambda
 
-not-apply : Bool @$\rightarrow$@ Bool
-not-appy b = not b          -- not use lambda
+@$\lambda$@+1 : @$\mathbb{N}$@ @$\rightarrow$@ @$\mathbb{N}$@
+@$\lambda$@+1 = (\n @$\rightarrow$@ suc n)   -- use lambda