# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1606656290 -32400
# Node ID ca656da4d4841a660f49d849f12a6e8fc7d02958
# Parent  af2428b97f6062ed3bacead8ddc431d085cb661a
...

diff -r af2428b97f60 -r ca656da4d484 FLComm.agda
--- a/FLComm.agda	Sun Nov 29 21:36:02 2020 +0900
+++ b/FLComm.agda	Sun Nov 29 22:24:50 2020 +0900
@@ -60,11 +60,14 @@
    comm3 (H ∷# []) (here refl) L3 = 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 )
    -- Any (_≡_ (perm→FL [ g , h ])) (tl3 G (cons H (cons a L1 x) x₁) L3)
-   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 L1 with tl3 G L1 (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3) | x∈FLins ( perm→FL [ FL→perm G , FL→perm H ] ) (tl3 G L1 (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))
-       ... | [] | m = {!!}
-       ... | cons a t x | m = subst (λ k → Any (_≡_ (perm→FL [ g , h ])) k ) ? (there m) 
+   comm3 (cons H L1 x₁) (here refl) L3 = comma L1 L3 where
+       commb : (a : FL n) → (L1 L3 : FList n) → (xr : fresh (FL n) ⌊ _f<?_ ⌋ a L1 )
+           → Any (_≡_ (perm→FL [ g , h ])) (tl3 G L1 (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))
+           → Any (_≡_ (perm→FL [ g , h ])) (tl3 G (cons a L1 xr) (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))
+       commb a L1 L3 xr wh = {!!}
+       comma :  (L1 L3 : FList n)  →  Any (_≡_ (perm→FL [ g , h ])) (tl3 G L1 (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))
+       comma [] L3 = 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 xr) L3 = commb a L1 L3 xr (comma L1 L3)
    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