Mercurial > hg > Members > kono > Proof > galois

changeset 222:9f86424a09b1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix to ≡_ in Any
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 07 Dec 2020 06:59:38 +0900
parents 14b518eecf82
children 9da456c2bfe3
files FLComm.agda FLutil.agda
diffstat 2 files changed, 58 insertions(+), 50 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Sun Dec 06 13:11:25 2020 +0900
+++ b/FLComm.agda	Mon Dec 07 06:59:38 2020 +0900
@@ -50,13 +50,13 @@
 record AnyFL (n : ℕ) (p : FL n) : Set where
    field
      anyList : FList n
-     anyP : (x : FL n) → p f≤ x →  Any ( _≡ x ) anyList 
+     anyP : (x : FL n) → p f≤ x →  Any (x ≡_ ) anyList 
 
 open import fin
 open AnyFL
 anyFL : (n : ℕ ) → AnyFL n FL0
 anyFL zero = record { anyList =  f0 ∷# []  ; anyP = any00 } where
-   any00 : (p : FL zero) →  FL0 f≤ p → Any (_≡ p) (f0 ∷# [])
+   any00 : (p : FL zero) →  FL0 f≤ p → Any (p ≡_) (f0 ∷# [])
    any00 f0 (case1 refl) = here refl
 anyFL (suc n) = any01 n (anyList (anyFL n)) (anyP (anyFL n) FL0 (case1 refl) ) {!!} where
    -- any03 : AnyFL (suc n) (fromℕ< a<sa :: fmax) → AnyFL (suc n) FL0
@@ -66,7 +66,7 @@
    any02 (suc i) (s≤s i<n) a any = any02 i (<-trans i<n a<sa) a record { anyList = cons ((fromℕ< (s≤s i<n )) :: a) (anyList any) any07 ; anyP = any08 } where
       any07 : fresh (FL (suc n)) ⌊ _f<?_ ⌋ (fromℕ< (s≤s i<n) :: a) (anyList any)
       any07 = {!!}
-      any08 : (x : FL (suc n)) → (fromℕ< (<-trans i<n a<sa) :: a) f≤ x → Any (_≡ x) (cons (fromℕ< (s≤s i<n) :: a) (anyList any) any07 )
+      any08 : (x : FL (suc n)) → (fromℕ< (<-trans i<n a<sa) :: a) f≤ x → Any (x ≡_) (cons (fromℕ< (s≤s i<n) :: a) (anyList any) any07 )
       any08 = {!!}
    -- loop on a 
    any03 :  (L : FList n) → (a : FL n) →  fresh (FL n) ⌊ _f<?_ ⌋ a L  →  AnyFL (suc n) (fromℕ< a<sa :: a ) → AnyFL (suc n) FL0
@@ -74,12 +74,12 @@
    any03 (cons b L br) a ( Data.Product._,_ (Level.lift a<b)_) any = any03 L b br record { anyList = anyList any04 ; anyP = any05 } where
       any04 : AnyFL (suc n) (zero :: a)
       any04 = any02 n a<sa a any
-      any05 : (x : FL (suc n)) → (fromℕ< a<sa :: b) f≤ x → Any (_≡ x) (anyList any04) -- 0<fmax : zero Data.Fin.< fromℕ< a<sa
+      any05 : (x : FL (suc n)) → (fromℕ< a<sa :: b) f≤ x → Any (x ≡_) (anyList any04) -- 0<fmax : zero Data.Fin.< fromℕ< a<sa
       any05 x mb≤x  = anyP any04 x (any06 a b x (toWitness a<b) mb≤x) where
          any06 : {n : ℕ } → (a b : FL n) → (x : FL (suc n)) → a f< b → (fromℕ< {n} a<sa :: b) f≤ x → (zero :: a) f≤ x 
          any06 {suc n} a b x a<b (case1 refl) = case2 (f<n 0<fmax)
          any06 {suc n} a b x a<b (case2 mb<x) = case2 (f<-trans (f<n 0<fmax) mb<x) 
-   any01 : (i : ℕ ) → (L : FList n) → Any (_≡ FL0) L → AnyFL (suc n) fmax → AnyFL (suc n) FL0 
+   any01 : (i : ℕ ) → (L : FList n) → Any (FL0 ≡_) L → AnyFL (suc n) fmax → AnyFL (suc n) FL0 
    any01 zero [] ()
    any01 (suc i) [] ()
    any01 zero (cons a L x)    _ any = {!!}
@@ -104,7 +104,7 @@
 record AnyComm (P Q : FList n) : Set where
    field
      commList : FList n
-     commAny : (p q : FL n) → Any (p ≡_) P →  Any (q ≡_) Q → Any ( _≡ perm→FL [ FL→perm p , FL→perm q ] ) commList
+     commAny : (p q : FL n) → Any ( p ≡_ ) P →  Any ( q ≡_ ) Q → Any (perm→FL [ FL→perm p , FL→perm q ] ≡_) commList
 
 open AnyComm -- q₂
 anyComm : (P Q : FList n) → AnyComm P Q
@@ -112,29 +112,37 @@
 anyComm [] (cons q Q qr) = record { commList = [] ; commAny = λ _ _ () }
 anyComm (cons p P pr) [] = record { commList = [] ; commAny = λ _ _ _ () }
 anyComm (cons p P pr) (cons q Q qr) = anyc0n Q where
-  insAnyComm : {p₁ q₁ h : FL n } → (xs : FList n)  → Any ( perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_ ) xs
-        → Any (perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_ ) (FLinsert h xs)
+  insAnyComm : {p₁ q₁ h : FL n } → (xs : FList n)  → Any (perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_) xs
+        → Any (perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_) (FLinsert h xs)
   insAnyComm xs any = insAny _ any
-  anyc04 : (x b : FL n) → (L : FList n) → Any (x ≡_ )  L → Any (x ≡_ )  (FLinsert b L)
+  anyc04 : (x b : FL n) → (L : FList n) → Any (x ≡_)  L → Any (x ≡_)  (FLinsert b L)
   anyc04 a b L any = insAny L any
 
   anyc0n : (Q1 : FList n) → AnyComm (cons p P pr) (cons q Q qr)
-  anyc01 :  (Q1 : FList n)  (q₁ : FL n) → (qr₁ : fresh (FL n) ⌊ _f<?_ ⌋ q₁ Q1 ) → (p₁ q₂ : FL n) → Any (_≡_ p₁) (cons p P pr) → Any (_≡_ q₂) (cons q Q qr) →
-    Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q₂ ]) (FLinsert (perm→FL [ FL→perm p , FL→perm q₁ ])  (commList (anyc0n Q1)) ) 
+  anyc01 :  (Q1 : FList n)  (q₁ : FL n) → (qr₁ : fresh (FL n) ⌊ _f<?_ ⌋ q₁ Q1 ) → (p₁ q₂ : FL n) → Any (p₁ ≡_) (cons p P pr) → Any (q₂ ≡_) (cons q Q qr) →
+    Any (perm→FL [ FL→perm p₁ , FL→perm q₂ ] ≡_) (FLinsert (perm→FL [ FL→perm p , FL→perm q₁ ])  (commList (anyc0n Q1)) ) 
   anyc01 [] q₁ qr₁ p₁ q₂ (here refl) (here refl) = {!!}
   anyc01 [] q₁ qr₁ p₁ q₂ (here refl) (there anyq) with anyc04 (perm→FL [ FL→perm p , FL→perm q₁ ]) (perm→FL [ FL→perm p , FL→perm q₁ ]) (commList (anyc0n [])) {!!}
   ... | t = {!!}
   anyc01 [] q₁ qr₁ p₁ q₂ (there anyp) (here refl) =  {!!} 
   anyc01 [] q₁ qr₁ p₁ q₂ (there anyp) (there anyq) = {!!} --  insAny (commList (anyc0n [])) {!!}  -- (commAny (anyc0n [])  p₁  q₂ (here refl) (there anyq) )
   anyc01 (cons q₃ Q1 qr₃) q₁ qr₁ p₁ q₂ anyp anyq = {!!}
-  anyc0n [] = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P (cons q Q qr))) ; commAny = anyc03 P Q } where
-    anyc03 :  (P Q : FList n) → (p₁ q₁ : FL n) → Any (_≡_ p₁) (cons p P {!!} ) → Any (_≡_ q₁) (cons q Q {!!}) → Any (_≡ perm→FL [ FL→perm p₁ , FL→perm q₁ ]) (FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P (cons q Q {!!}))))
-    anyc03 P Q p₁ q₁ (here refl) (here refl) = {!!}
-    anyc03 P Q p₁ q₁ (here refl) (there anyq) = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ (here refl) anyq ) 
-    anyc03 P Q p₁ q₁ (there anyp) (here refl) =  insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ anyp (here refl)) 
-    anyc03 P Q p₁ q₁ (there anyp) (there anyq) =  insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ anyp anyq ) 
+  anyc0n [] = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P (cons q Q qr))) ; commAny = {!!} } where
+    anyc03 :  (P Q : FList n) → (p₁ q₁ : FL n) 
+        → Any (p₁ ≡_) P → Any (q₁ ≡_) Q
+        → Any (perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_) (FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P Q))) 
+    anyc03 = {!!} where
+       anyc05 :  (P Q : FList n) → (p₁ q₁ : FL n) 
+           → Any (p₁ ≡_) P → Any (q₁ ≡_) Q → (x y : FL n) → ( z : FList n )
+           → Any (x ≡_) z 
+           → Any (x ≡_) (FLinsert y z) 
+       anyc05 P Q p₁ q₁ anyp anyq x y z anyz = {!!}
+       anyc07 : (x b : FL n) → (L : FList n) → Any (x ≡_)  L → Any (x ≡_)  (FLinsert b L)
+       anyc07 a b L any = insAny L any
+       anyc06 : (x y : FL n) → ( z : FList n ) → Any (x ≡_) z → Any (x ≡_) (FLinsert y z) 
+       anyc06 x y z anyz = insAny  z anyz
   anyc0n (cons q₁ Q1 qr₁ ) = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q₁ ]) (commList (anyc0n Q1)) 
-                                 ; commAny = anyc01 Q1 q₁ qr₁ }
+                                 ; commAny = {!!}  }
 
 -- {-# TERMINATING #-}
 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )
@@ -144,53 +152,53 @@
    H = perm→FL h
 
    -- tl3 case
-   commc :  (L3 L1 : FList n) →  Any (_≡_ (perm→FL [  FL→perm G , FL→perm H ])) L3 
-           →  Any (_≡_ (perm→FL [ FL→perm G , FL→perm H ])) (tl3 G L1 L3)
+   commc :  (L3 L1 : FList n) →  Any ((perm→FL [  FL→perm G , FL→perm H ]) ≡_) L3 
+           →  Any ((perm→FL [ FL→perm G , FL→perm H ]) ≡_) (tl3 G L1 L3)
    commc L3 [] any = any
    commc L3 (cons a L1 _) any = commc (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) L3) L1 (insAny _ any)
    comm6 : perm→FL [ FL→perm G , FL→perm H ] ≡ perm→FL [ g , h ]
    comm6 = pcong-pF (comm-resp (FL←iso _) (FL←iso _))  
-   comm3 : (L1 : FList n) → Any (H ≡_) L1 → (L3 : FList n) → Any (_≡_ (perm→FL [ g , h ])) (tl3 G L1 L3)
-   comm3 (H ∷# []) (here refl) L3 = subst (λ k → Any (_≡_  k) (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3 ) )
+   comm3 : (L1 : FList n) → Any (H ≡_) L1 → (L3 : FList n) → Any ((perm→FL [ g , h ]) ≡_) (tl3 G L1 L3)
+   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 )
-   comm3 (cons H L1 x₁) (here refl) L3 = subst (λ k → Any (_≡_ k) (tl3 G L1 (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))) comm6
+   comm3 (cons H L1 x₁) (here refl) L3 = subst (λ k → Any (k ≡_) (tl3 G L1 (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))) comm6
        (commc (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3 ) L1 (x∈FLins ( perm→FL [ FL→perm G , FL→perm H ] ) L3))
    comm3 (cons a L  _) (there b) L3 = comm3 L b (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) L3)
 
    -- tl2 case
-   comm2 : (L L1 : FList n) → Any (G ≡_) L → Any (H ≡_) L1 → (L3 : FList n) → Any (perm→FL [ g , h ]  ≡_) (tl2 L L1 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
        comm8 : (L L4 L2 : FList n) → (a : FL n) 
-            → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2)
-            → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L L2))
+            → Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 L2)
+            → Any ((perm→FL [ g , h ]) ≡_ ) (tl2 L4 L1 (tl3 a L L2))
        comm8← : (L L4 L2 : FList n) → (a : FL n)  → ¬ ( a ≡ perm→FL g )
-           →  Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L L2))
-           →  Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2)
+           →  Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 (tl3 a L L2))
+           →  Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 L2)
        comm9← : (L4 L2 : FList n) → (a a₁ : FL n) → ¬ ( a ≡ perm→FL g )
-           → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))
-           → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2) 
-       --  Any (_≡_ (perm→FL [ g , h ])) (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2) → Any (_≡_ (perm→FL [ g , h ])) L2
+           → Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))
+           → Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 L2) 
+       --  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₁ 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))
-       -- Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2)
-       -- Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a₂ L1 L2))
+       -- 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))
+       -- Any (_≡ (perm→FL [ g , h ])) (tl2 L4 L1 L2)
+       -- Any (_≡ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a₂ L1 L2))
        comm8← [] L4 L2 a _ any = any 
        comm8← (cons a₁ L x) L4 L2 a not any  = comm8← L  L4 L2 a not
-            (comm9← L4 (tl3 a L L2 ) a a₁ not (subst (λ k →  Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1  k )) {!!} any ))
-       -- Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L (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₁ ]) (tl3 a L L2)))
-       comm9 : (L4 L2 : FList n) → (a a₁ : FL n) → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 L2) →
-                                                   Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))
+            (comm9← L4 (tl3 a L L2 ) a a₁ not (subst (λ k →  Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1  k )) {!!} any ))
+       -- Any (_≡ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L (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₁ ]) (tl3 a L L2)))
+       comm9 : (L4 L2 : FList n) → (a a₁ : FL n) → Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 L2) →
+                                                   Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))
        comm8 [] L4 L2 a any = any
        comm8 (cons a₁ L x) L4 L2 a any =  comm8 L  L4 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2) a  (comm9 L4 L2 a a₁ any)
        comm9 [] L2 a a₁ any = insAny _ any
        comm9 (cons a₂ L4 x) L2 a a₁ any = comm8 L1 L4 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2) a₂ (comm9 L4 L2 a a₁ (comm8← L1 L4 L2 a₂ {!!} any))
        -- found g, we have to walk thru till the end
-       comm7 : (L L3 : FList n) → Any (_≡_ (perm→FL [ g , h ])) (tl2 L L1 (tl3 G L1 L3))
+       comm7 : (L L3 : FList n) → Any ((perm→FL [ g , h ]) ≡_) (tl2 L L1 (tl3 G L1 L3))
        -- at the end, find h
        comm7 [] L3 = comm3 L1 b L3  
        -- add n path
--- a/FLutil.agda	Sun Dec 06 13:11:25 2020 +0900
+++ b/FLutil.agda	Mon Dec 07 06:59:38 2020 +0900
@@ -293,7 +293,7 @@
 open import Data.List.Fresh.Relation.Unary.Any 
 open import Data.List.Fresh.Relation.Unary.All 
 
-x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n)  → Any (x ≡_ ) (FLinsert x xs)
+x∈FLins : {n : ℕ} → (x : FL n ) → (xs : FList n)  → Any (x ≡_) (FLinsert x xs)
 x∈FLins {zero} f0 [] = here refl
 x∈FLins {zero} f0 (cons f0 xs x) = here refl
 x∈FLins {suc n} x [] = here refl
@@ -303,11 +303,11 @@
 x∈FLins {suc n} x (cons a [] x₁)              | tri> ¬a ¬b a<x = there ( here refl )
 x∈FLins {suc n} x (cons a (cons a₁ xs x₂) x₁) | tri> ¬a ¬b a<x = there ( x∈FLins x (cons a₁ xs x₂) )
 
-nextAny : {n : ℕ} → {x h : FL n } → {L : FList n}  → {hr : fresh (FL n) ⌊ _f<?_ ⌋ h L } → Any (x ≡_ ) L → Any (x ≡_ ) (cons h L hr )
+nextAny : {n : ℕ} → {x h : FL n } → {L : FList n}  → {hr : fresh (FL n) ⌊ _f<?_ ⌋ h L } → Any (x ≡_) L → Any (x ≡_) (cons h L hr )
 nextAny (here x₁) = there (here x₁)
 nextAny (there any) = there (there any)
 
-insAny : {n : ℕ} → {x h : FL n } → (xs : FList n)  → Any (x ≡_ ) xs → Any (x ≡_ ) (FLinsert h xs)
+insAny : {n : ℕ} → {x h : FL n } → (xs : FList n)  → Any (x ≡_) xs → Any (x ≡_) (FLinsert h xs)
 insAny {zero} {f0} {f0} (cons a L xr) (here refl) = here refl
 insAny {zero} {f0} {f0} (cons a L xr) (there any) = insAny {zero} {f0} {f0} L any 
 insAny {suc n} {x} {h} (cons a L xr) any with FLcmp h a 
@@ -318,23 +318,23 @@
 insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (there any) | tri> ¬a ¬b c = there (insAny (cons a₁ L x₁) any)
 
 {-# TERMINATING #-}
-AnyFList : {n : ℕ }  → (x : FL n ) →  Any (x ≡_ ) (∀Flist fmax)
+AnyFList : {n : ℕ }  → (x : FL n ) →  Any (x ≡_) (∀Flist fmax)
 AnyFList {zero} f0 = here refl
 AnyFList {suc zero} (zero :: f0) = here refl
-AnyFList {suc (suc n)} (x :: y) = subst (λ k → Any (_≡_ (k :: y)) (Flist (suc n) a<sa (∀Flist fmax) (∀Flist fmax) ))
+AnyFList {suc (suc n)} (x :: y) = subst (λ k → Any ((k :: y) ≡_) (Flist (suc n) a<sa (∀Flist fmax) (∀Flist fmax) ))
          (fromℕ<-toℕ _ _) ( AnyFList1 (suc n) (toℕ x) a<sa (∀Flist fmax) (∀Flist fmax) fin<n fin<n (AnyFList y) (AnyFList y)) where
    AnyFList1 :  (i x : ℕ) → (i<n : i < suc (suc n) ) → (L L1 : FList (suc n) ) → (x<n : x < suc (suc n) ) → x < suc i
-        → Any (y ≡_ ) L → Any (y ≡_ ) L1
-        → Any (((fromℕ< x<n) :: y) ≡_ ) (Flist i i<n L L1)
+        → Any (y ≡_) L → Any (y  ≡_) L1
+        → Any (((fromℕ< x<n) :: y) ≡_) (Flist i i<n L L1)
    AnyFList1 zero x i<n [] L1 (s≤s x<i) _ () _
    AnyFList1 zero zero i<n (cons y L xr) L1 x<n (s≤s z≤n) (here refl) any = x∈FLins (zero :: y) (Flist 0 i<n L L1)
    AnyFList1 zero zero i<n (cons a L xr) L1 x<n (s≤s z≤n) (there wh) any = insAny _ (AnyFList1 zero zero i<n L L1 x<n (s≤s z≤n) wh any)
    AnyFList1 (suc i) x (s≤s i<n) (cons y L x₁) L1 x<n (s≤s x<i) (here refl) any with <-fcmp (fromℕ< x<n) (fromℕ< (s≤s i<n))
    ... | tri< a ¬b ¬c = insAny  (Flist (suc i) (s≤s i<n) L L1) (af1 L ) where
-        af1 : (L : FList (suc n)) → Any (_≡_ (fromℕ< x<n :: y)) (Flist (suc i) (s≤s i<n) L L1)
+        af1 : (L : FList (suc n)) → Any ((fromℕ< x<n :: y) ≡_) (Flist (suc i) (s≤s i<n) L L1)
         af1 [] = AnyFList1 i x (<-trans i<n a<sa) L1 L1 x<n (subst₂ (λ j k → j < k )  (toℕ-fromℕ< _) (cong suc  (toℕ-fromℕ< _)) a )  any any
         af1 (cons a L x) = insAny (Flist (suc i) (s≤s i<n) L L1) (af1 L )
-   ... | tri≈ ¬a b ¬c = subst (λ k → Any (_≡_ (fromℕ< x<n :: y)) (FLinsert k  (Flist (suc i) (s≤s i<n) L L1) )) (cong (λ k → k :: y) b)
+   ... | tri≈ ¬a b ¬c = subst (λ k → Any ((fromℕ< x<n :: y) ≡_) (FLinsert k  (Flist (suc i) (s≤s i<n) L L1) )) (cong (λ k → k :: y) b)
         (x∈FLins (fromℕ< x<n :: y) (Flist (suc i) (s≤s i<n) L L1))
    ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> x<i (subst₂ (λ j k → suc (suc k) ≤ j ) (toℕ-fromℕ< _) (toℕ-fromℕ< _) c) )
    AnyFList1 (suc i) x (s≤s i<n) (cons a (cons a₁ L x₂) x₁) L1 x<n (s≤s x<i) (there wh) any with FLcmp a a₁