# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1606610176 -32400
# Node ID f9aa8bb5fb1d367b18f91fba5ad11194b12a5335
# Parent  a670644d5624070b96c4e047c6a538dc4d26cfa6
...

diff -r a670644d5624 -r f9aa8bb5fb1d FLComm.agda
--- a/FLComm.agda	Sun Nov 29 09:24:30 2020 +0900
+++ b/FLComm.agda	Sun Nov 29 09:36:16 2020 +0900
@@ -63,11 +63,9 @@
    comm3 (cons H L1 x₁) (here refl) L3 = comma L1 where
        comma :  (L1 : FList n)  →  Any (_≡_ (perm→FL [ g , h ])) (tl3 G L1 (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))
        comma [] = subst (λ k → Any (_≡_  k) (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3 ) ) comm6 (x∈FLins ( perm→FL [ FL→perm G , FL→perm H ] ) L3 )
-       comma (cons a L1 x) = {!!} where -- Any (_≡_ (perm→FL [ g , h ])) (tl3 G (cons a L2 x) (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))
-          commb :  Any (_≡_ (perm→FL [ g , h ]))
-               (tl3 (perm→FL g) L1 (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) L1 )))
-          commb with x∈FLins  (perm→FL [ FL→perm G , FL→perm a ]) (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) L1 ))
-          ... | t = {!!}
+       comma (cons a L1 x) = {!!} where -- Any (_≡_ (perm→FL [ g , h ])) (tl3 G (cons a L1 x) (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))
+          commb :                          Any (_≡_ (perm→FL [ g , h ])) (tl3 G L1            (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3)) 
+          commb = comma L1
    comm3 (cons a L  _) (there b) L3 = comm3 L b (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) L3)
    comm2 : (L L1 : FList n) → Any (G ≡_) L → Any (H ≡_) L1 → (L3 : FList n) → Any (perm→FL [ g , h ]  ≡_) (tl2 L L1 L3)
    comm2 (cons G L xr) L1 (here refl) b L3 = comm7 L L3 where