--- a/FLComm.agda	Sat Nov 28 10:08:51 2020 +0900
+++ b/FLComm.agda	Sat Nov 28 21:50:16 2020 +0900
@@ -25,6 +25,7 @@
 
 -- infixr  100 _::_
 
+open import Relation.Nary using (⌊_⌋)
 open import Data.List.Fresh hiding ([_])
 open import Data.List.Fresh.Relation.Unary.Any
 
@@ -49,13 +50,15 @@
 
 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )
 CommStage→ zero x (Level.lift tt) = AnyFList (perm→FL x)
-CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 (CommFListN i) (CommFListN i) (CommStage→ i g p) (CommStage→ i h q) where
+CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 (CommFListN i) (CommFListN i) (CommStage→ i g p) (CommStage→ i h q) [] where
    G = perm→FL g
    H = perm→FL h
-   comm2 : (L L1 : FList n) → Any (G ≡_) L → Any (H ≡_) L1 → Any (perm→FL [ g , h ]  ≡_) (tl2 L L1 [])
-   comm2 (cons G L xr) (cons H L1 yr) (here refl) (here refl) = {!!}
-   comm2 (cons x L xr) (cons y L1 yr) (here x₁) (there b) = {!!}
-   comm2 (cons x L xr) (cons y L1 yr) (there a) b = {!!}
+   comm3 : (L L1 : FList n) → (xr : fresh (FL n) ⌊ _f<?_ ⌋ G L ) → Any (H ≡_) L1 → (L3 : FList n) → Any (_≡_ (perm→FL [ g , h ])) (tl2 (cons G L xr) L1 L3)
+   comm3 [] L1 _ b L3 = {!!}
+   comm3 (cons a L x) L1 _ b 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 = comm3 L L1 xr b L3
+   comm2 (cons x L xr) L1 (there a) b L3 = comm2 L L1 a b {!!}
 CommStage→ (suc i) x (ccong {f} {x} eq p) = subst (λ k → Any (k ≡_) (tl2 (CommFListN i) (CommFListN i) [])) (comm4 eq) (CommStage→ (suc i) f p ) where
    comm4 : f =p= x →  perm→FL f ≡ perm→FL x
    comm4 = pcong-pF