# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598949933 -32400
# Node ID e435dbe2e7a6dd1b727ce6219be0e364a31d8d95
# Parent  2d0738a38ac963b16b4c368eca12aaf4a9fa08ad
...

diff -r 2d0738a38ac9 -r e435dbe2e7a6 Putil.agda
--- a/Putil.agda	Tue Sep 01 17:21:31 2020 +0900
+++ b/Putil.agda	Tue Sep 01 17:45:33 2020 +0900
@@ -586,6 +586,10 @@
  
 t6 = perm→FL t4
 
+----
+--  if n is fixed, perm→FL ( FL→perm fl ) ≡ fl is refl for each concrete fl
+--  so we may prove this easily by co-induction
+--
 FL→iso : {n : ℕ }  → (fl : FL n )  → perm→FL ( FL→perm fl ) ≡ fl
 FL→iso f0 = refl
 FL→iso {suc n} (x :: fl) = cong₂ ( λ j k → j :: k ) f001 f002 where
@@ -634,12 +638,14 @@
 FL←iso {0} perm = record { peq = λ () }
 FL←iso {suc n} perm with  perm→FL perm | inspect  perm→FL perm
 ... | x :: fl | record { eq = e } = ptrans (pcong-Fp e ) f004 where
-    f004 :    FL→perm ( x :: fl ) =p= perm 
+    f003 : perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm)) ≡ fl
+    f003 = {!!}
+    f004 : FL→perm ( x :: fl ) =p= perm 
     f004 = record { peq = λ q → ( begin
         (pprep (FL→perm fl)  ∘ₚ pins ( toℕ≤pred[n] x ))  ⟨$⟩ʳ q
-     ≡⟨ {!!}  ⟩
+     ≡⟨ cong (λ k →  (pprep (FL→perm  k)  ∘ₚ pins ( toℕ≤pred[n] x ))  ⟨$⟩ʳ q ) (sym f003 ) ⟩
         (pprep (FL→perm (perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) )))  ∘ₚ pins ( toℕ≤pred[n] x ))  ⟨$⟩ʳ q
-     ≡⟨ {!!}  ⟩
+     ≡⟨ peq (presp (pprep-cong (FL←iso _ ) ) prefl ) q ⟩
         (pprep (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm))   ∘ₚ pins ( toℕ≤pred[n] x ))  ⟨$⟩ʳ q
      ≡⟨ {!!}  ⟩
         perm ⟨$⟩ʳ q