# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1607639889 -32400
# Node ID 80b9fb5f80ab020fba237d0321226aad4944fbd0
# Parent  d8f6d04edbbcffe78061d70e1db7b23fd580e187
slightly better

diff -r d8f6d04edbbc -r 80b9fb5f80ab FLComm.agda
--- a/FLComm.agda	Thu Dec 10 19:15:25 2020 +0900
+++ b/FLComm.agda	Fri Dec 11 07:38:09 2020 +0900
@@ -180,7 +180,7 @@
 record AnyFin (n : ℕ)  : Set where
    field
      allFin : FList (suc n)
-     anyF : {i : ℕ} → (i<n : i < suc n) → Any (fromℕ< i<n :: FL0 ≡_ ) allFin 
+     anyF : (x : Fin (suc n)) → Any (x :: FL0 ≡_ ) allFin 
 
 open AnyFin
 
@@ -188,27 +188,27 @@
 anyFL01 zero    = record { allFL = (zero :: f0) ∷# [] ; anyP = λ x → anyFL2 x ((zero :: f0) ∷# []) refl } 
 anyFL01 (suc n) = record { allFL = commList anyC ;  anyP =  anyFL02 } where
      anyFL04 :  (n : ℕ) → AnyFin n
-     anyFL04 n = record { allFin = anyFL05 a<sa ; anyF = λ {j} j<n → anyFL06 {n} {j} a<sa j<n (anyFL07 j<n) } where 
-         anyFL08 : {i n : ℕ } (i<n : suc i ≤ n) (j<n : suc (suc i) ≤ suc n) → fromℕ< (≤-pred j<n) ≡ fromℕ< i<n
-         anyFL08 {zero} {.(suc _)} (s≤s z≤n) (s≤s (s≤s j<n)) = refl
-         anyFL08 {suc i} {.(suc _)} (s≤s i<n) (s≤s j<n) = cong (λ k → suc k ) (anyFL08 (i<n) (j<n) )
-         anyFL07 : {j : ℕ } → j < suc n → j ≤ n
-         anyFL07 (s≤s j<n) = j<n
+     anyFL04 n = record { allFin = anyFL05 a<sa ; anyF = λ x → anyFL06 a<sa x fin<n } where 
+         anyFL08 : {n i : ℕ} {x : Fin (suc n)} {i<n : suc i < suc n}  → toℕ x ≡ suc i → x ≡ suc (fromℕ< (≤-pred i<n))
+         anyFL08 {n} {i} {x} {i<n} eq = toℕ-injective ( begin
+                toℕ x                               ≡⟨ eq ⟩
+                suc i                               ≡⟨ cong suc (≡-sym (toℕ-fromℕ< _ )) ⟩
+                suc (toℕ (fromℕ< (≤-pred i<n)) )
+          ∎ ) where open ≡-Reasoning
          anyFL05 : {i : ℕ} → (i < suc n) → FList (suc n)
          anyFL05 {0} (s≤s z≤n) = zero :: FL0 ∷# []
          anyFL05 {suc i} (s≤s i<n) = FLinsert (fromℕ< (s≤s i<n) :: FL0) (anyFL05 {i} (<-trans i<n a<sa))
-         anyFL06 : {i j : ℕ} (i<n : i < suc n) → (j<n : j < suc n) → (j≤i : j ≤ i) → Any (_≡_ (fromℕ< j<n :: FL0)) (anyFL05 i<n)
-         anyFL06 {0} {zero} (s≤s z≤n) j<n j≤i = here refl
-         anyFL06 {suc i} {0} (s≤s i<n) j<n j≤i = insAny _ (anyFL06 {i} {0} (<-trans i<n a<sa) j<n z≤n)
-         anyFL06 {suc i} {j} (s≤s i<n) j<n (s≤s j≤i) with <-cmp j (suc i)
-         ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (s≤s j≤i) c) 
-         ... | tri< (s≤s a) ¬b ¬c = insAny _ (anyFL06 {i} {j} (<-trans i<n a<sa) j<n a)
-         ... | tri≈ ¬a refl ¬c = subst (λ k →  Any (_≡_ _) (FLinsert (suc k :: FL0) (anyFL05 (<-trans i<n a<sa))) ) (anyFL08 i<n j<n)
-              (x∈FLins  (suc (fromℕ< (≤-pred j<n)) :: FL0) (anyFL05 (<-trans i<n a<sa)))
+         anyFL06 : {i : ℕ} → (i<n : i < suc n) → (x : Fin (suc n)) → toℕ x < suc i → Any (_≡_ (x :: FL0)) (anyFL05 i<n)
+         anyFL06 (s≤s z≤n) zero (s≤s lt) = here refl
+         anyFL06 {suc i} (s≤s (s≤s i<n)) x (s≤s lt) with <-cmp (toℕ x) (suc i)
+         ... | tri< a ¬b ¬c = insAny _ (anyFL06 (<-trans (s≤s i<n) a<sa) x a) 
+         ... | tri≈ ¬a b ¬c = subst (λ k →  Any (_≡_ (x :: FL0)) (FLinsert (k :: FL0) (anyFL05 {i} (<-trans (s≤s i<n) a<sa))))
+                  (anyFL08 {n} {i} {x} {s≤s (s≤s i<n)} b) (x∈FLins (x :: FL0)  (anyFL05 {i} (<-trans (s≤s i<n) a<sa)))
+         ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c (s≤s lt) )
      anyC = anyComm (allFin (anyFL04 (suc n))) (allFL (anyFL01 n)) (λ p q → FLpos p :: q )
      anyFL02 : (x : FL (suc (suc n))) → Any (_≡_ x) (commList anyC)
      anyFL02 (x :: y) = commAny anyC (x :: FL0) y
-                       (subst (λ k → Any (_≡_ (k :: FL0) ) _) (fromℕ<-toℕ _ _) (anyF (anyFL04 (suc n)) x≤n )) (anyP (anyFL01 n) y) where
+                       (subst (λ k → Any (_≡_ (k :: FL0) ) _) (fromℕ<-toℕ _ _) (anyF (anyFL04 (suc n)) (fromℕ< x≤n) )) (anyP (anyFL01 n) y) where
          x≤n : suc (toℕ x)  ≤ suc (suc n)
          x≤n = toℕ<n x