# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1606947082 -32400
# Node ID a180e6d4bfd67a90284ae6d7da0082348c1fee0c
# Parent  5ca41a11f8ae2e28c977735d23a1390b7a292b39
...

diff -r 5ca41a11f8ae -r a180e6d4bfd6 FLComm.agda
--- a/FLComm.agda	Wed Dec 02 11:49:05 2020 +0900
+++ b/FLComm.agda	Thu Dec 03 07:11:22 2020 +0900
@@ -86,7 +86,7 @@
        --  Any (_≡_ (perm→FL [ g , h ])) (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2) → Any (_≡_ (perm→FL [ g , h ])) L2
        comm9← [] L2 a a₁ not any = {!!}
        comm9← (cons a₂ L4 x) L2 a a₁ not any = comm8 L1 L4 L2 a₂
-           (comm9← L4 L2 a a₁ {!!}
+           (comm9← L4 L2 a a₁ not
            (comm8← L1 L4 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2 ) a₂ {!!} any)) 
        -- Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a₂ L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))) →
        -- Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))