# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598248227 -32400
# Node ID 3825082ebdbd73e017008a1c3010594a511e346a
# Parent  442873eaf80b7d24b02e7fa8bfec307f1c6f09c2
∀-FL : (n : ℕ ) → List (FL (suc n))

diff -r 442873eaf80b -r 3825082ebdbd Putil.agda
--- a/Putil.agda	Mon Aug 24 14:40:11 2020 +0900
+++ b/Putil.agda	Mon Aug 24 14:50:27 2020 +0900
@@ -285,16 +285,17 @@
 lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
 lem2 i≤n = ≤-trans i≤n ( refl-≤s )
 
-∀-FL : {n : ℕ } → Fin n → List (FL n)
-∀-FL  x  = ∀-FL1 x  where
-    ∀-FL2 : { n : ℕ } → Fin (suc n) → (i : ℕ ) → i ≤ n → List (FL n)  → List (FL (suc n)) → List (FL (suc n))
-    ∀-FL2 y zero z≤n [] t = t
-    ∀-FL2 y zero z≤n (x ∷ fls) t = ∀-FL2 y zero z≤n fls (( zero :: x )  ∷ t ) 
-    ∀-FL2 y (suc i) (s≤s lt) [] t = t
-    ∀-FL2 y (suc i) (s≤s lt) (fl ∷ fls) t = ∀-FL2 y i (lem2 lt) (fl ∷ fls) (( fromℕ≤ (s≤s (s≤s lt)) :: fl )  ∷ t ) 
-    ∀-FL1 : {n : ℕ } → (Fin n) →  List (FL n) 
-    ∀-FL1 zero    = []
-    ∀-FL1 (suc x) =  ∀-FL2 (suc x) (toℕ x) (≤-trans refl-≤s fin<n ) ( ∀-FL1 x) []
+∀-FL : (n : ℕ ) → List (FL (suc n))
+∀-FL  x  = fls6 x  where
+   fls4 :  ( i n : ℕ ) → (i<n : i ≤ n ) → FL  n → List (FL  (suc n))  → List (FL  (suc n)) 
+   fls4 zero n i≤n perm x = (zero :: perm ) ∷ x
+   fls4 (suc i) n i≤n  perm x = fls4 i n (≤-trans refl-≤s i≤n ) perm ((fromℕ≤ (s≤s i≤n) :: perm ) ∷ x)
+   fls5 :  ( n : ℕ ) → List (FL n) → List (FL  (suc n))  → List (FL (suc n)) 
+   fls5 n [] x = x
+   fls5 n (h ∷ x) y = fls5  n x (fls4 n n lem0 h y)
+   fls6 :  ( n : ℕ ) → List (FL  (suc n)) 
+   fls6 zero = (zero :: f0) ∷ []
+   fls6 (suc n) =  fls5 (suc n) (fls6 n) []   
 
 all-perm : (n : ℕ ) → List (Permutation (suc n) (suc n) )
 all-perm n = pls6 n where