--- a/Putil.agda	Mon Aug 31 09:51:13 2020 +0900
+++ b/Putil.agda	Mon Aug 31 11:45:09 2020 +0900
@@ -511,7 +511,23 @@
 shrink-cong : { n : ℕ } → {x y : Permutation (suc n) (suc n)}
     → x =p= y
     → (x=0 :  x ⟨$⟩ˡ (# 0) ≡ # 0 ) → (y=0 : y ⟨$⟩ˡ (# 0) ≡ # 0 )  → shrink x x=0 =p=  shrink y y=0 
-shrink-cong {n} {x} {y} x=0 y=0  = {!!}
+shrink-cong {n} {x} {y} x=y x=0 y=0  = record  { peq = p002 } where
+    p002 : (q : Fin n) → (shrink x x=0 ⟨$⟩ʳ q) ≡ (shrink y y=0 ⟨$⟩ʳ q)
+    p002 q with x ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ x ) (suc q) | y ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ y ) (suc q)
+    p002 q | zero   | record { eq = ex } | zero   | ey                  = ⊥-elim ( sh1 x x=0 ex )
+    p002 q | zero   | record { eq = ex } | suc py | ey                  = ⊥-elim ( sh1 x x=0 ex )
+    p002 q | suc px | ex                 | zero   | record { eq = ey }  = ⊥-elim ( sh1 y y=0 ey )
+    p002 q | suc px | record { eq = ex } | suc py | record { eq = ey }  = p003 ( begin
+           suc px
+         ≡⟨ sym ex ⟩
+           x ⟨$⟩ʳ (suc q)
+         ≡⟨ peq x=y (suc q) ⟩
+           y ⟨$⟩ʳ (suc q)
+         ≡⟨ ey ⟩
+           suc py
+         ∎ ) where
+        p003 : suc px ≡ suc py → px ≡ py
+        p003 refl = refl
 
 FL→perm   : {n : ℕ }  → FL n → Permutation n n 
 FL→perm f0 = pid
@@ -544,7 +560,10 @@
 -- perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (remove (# 0) perm)  
 
 pcong-pF : {n : ℕ }  → {x y : Permutation n n}  → x =p= y → perm→FL x ≡ perm→FL y
-pcong-pF = {!!}
+pcong-pF {zero} eq = refl
+pcong-pF {suc n} {x} {y} eq = cong₂ (λ j k → j :: k ) ( peq eq (# 0)) (pcong-pF (shrink-cong (presp eq (record { peq = p-inv p001} )) (p=0 x) (p=0 y))) where
+    p001 : pins (toℕ≤pred[n] (x ⟨$⟩ʳ (# 0))) =p=  pins (toℕ≤pred[n] (y ⟨$⟩ʳ (# 0)))
+    p001 = {!!}
 
 -- t5 = plist t4 ∷ plist ( t4  ∘ₚ flip (pins ( n≤  3 ) ))
 t5 = plist (t4) ∷ plist (flip t4)