# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1598960498 -32400
# Node ID cb3281e8322993142edc6ebb9393bcb087c19752
# Parent  5d60a060453cec90f352e596e921ad04d2b22234
FL iso done

diff -r 5d60a060453c -r cb3281e83229 Putil.agda
--- a/Putil.agda	Tue Sep 01 20:00:24 2020 +0900
+++ b/Putil.agda	Tue Sep 01 20:41:38 2020 +0900
@@ -642,17 +642,13 @@
         FL→perm ( perm→FL perm  ) ⟨$⟩ʳ q
      ≡⟨⟩
         (pprep (FL→perm (perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) )))  ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ) ) ⟨$⟩ʳ q
-     ≡⟨  peq (presp (pprep-cong (FL←iso _ ) ) prefl ) q  ⟩
+     ≡⟨  peq (presp {suc n} {_} {_} {pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)))} (pprep-cong {n} {FL→perm (perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ))} (FL←iso _ ) ) prefl ) q  ⟩
          (pprep (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm))   ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))  ⟨$⟩ʳ q 
-     ≡⟨  peq (passoc _ _ _  ) q ⟩
-         (pprep (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm))) ⟨$⟩ʳ ((  pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))  ⟨$⟩ʳ q )
-     ≡⟨ peq (shrink-iso2 (p=0 perm)) ((pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))  ⟨$⟩ʳ q) ⟩
+     ≡⟨ peq (presp {suc n} {pprep (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm))} {perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))} {pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) )} (shrink-iso2 (p=0 perm)) prefl) q  ⟩
          ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))  ⟨$⟩ʳ q 
-     ≡⟨ peq (passoc _ _ _ ) q ⟩
-         (perm ∘ₚ (flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)))) ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) )))  ⟨$⟩ʳ q 
-     ≡⟨ {!!}  ⟩
+     ≡⟨ peq (presp {suc n} {perm} {_} {flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)))) ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)))} {pid} prefl record { peq = λ q → inverseʳ (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)))) }) q  ⟩
         ( perm ∘ₚ pid ) ⟨$⟩ʳ q
-     ≡⟨ {!!}  ⟩
+     ≡⟨⟩
         perm ⟨$⟩ʳ q
      ∎  ) }