--- a/presen.html	Sat Jan 09 09:43:12 2021 +0900
+++ b/presen.html	Sat Jan 09 18:02:41 2021 +0900
@@ -499,6 +499,39 @@
 ここにあったら here、先にあるなら there
 <p>
 
+<pre>
+    Any (x ≡_) (FLinsert x xs)
+
+</pre>
+という形で使う。
+<pre>
+      x ≡_
+
+</pre>
+は
+<pre>
+      λ y → x ≡ y
+
+</pre>
+
+のこと。  _≡_ x と書いても良い。
+<p>
+ちなみに、
+<pre>
+      x _≡
+
+</pre>
+は
+<pre>
+      λ y → y ≡ x
+
+</pre>
+
+なので意味が異なる (≡は対称なので結局は同じなのだが、Agda の推論はそこまでカバーしない)
+<p>
+これで三日くらい悩みました
+<p>
+
 <hr/>
 <h2><a name="content023">Fresh List :        Insert</a></h2>
 普通の insert と変わらないけど、fresh を作る必要がある
@@ -653,6 +686,8 @@
 <p>
 型検査時に compile して計算する機能はない
 <p>
+これが証明に接続されると、5次が可解でないことはわかるが、その理由はわからない。不可解な証明だということになる。
+<p>
 
 <hr/>
 <h2><a name="content031">Analysis :        overhead of proof carrying data structure</a></h2>
@@ -983,5 +1018,5 @@
 <li><a href="#content039">  sym5</a>
 </ol>
 
-<hr/> Shinji KONO <kono@ie.u-ryukyu.ac.jp> /  Fri Jan  8 15:30:18 2021
+<hr/> Shinji KONO <kono@ie.u-ryukyu.ac.jp> /  Sat Jan  9 09:54:59 2021
 </body></html>

--- a/presen.ind	Sat Jan 09 09:43:12 2021 +0900
+++ b/presen.ind	Sat Jan 09 18:02:41 2021 +0900
@@ -354,6 +354,22 @@
 
 ここにあったら here、先にあるなら there
 
+    Any (x ≡_) (FLinsert x xs)
+
+という形で使う。
+      x ≡_
+は
+      λ y → x ≡ y
+のこと。  _≡_ x と書いても良い。
+
+ちなみに、
+      x _≡
+は
+      λ y → y ≡ x
+なので意味が異なる (≡は対称なので結局は同じなのだが、Agda の推論はそこまでカバーしない)
+
+これで三日くらい悩みました
+
 --Fresh List :        Insert
 
 普通の insert と変わらないけど、fresh を作る必要がある
@@ -467,6 +483,8 @@
 
 型検査時に compile して計算する機能はない
 
+これが証明に接続されると、5次が可解でないことはわかるが、その理由はわからない。
+不可解な証明だということになる。
 
 --Analysis :        overhead of proof carrying data structure