--- a/Putil.agda	Wed Aug 26 23:53:40 2020 +0900
+++ b/Putil.agda	Thu Aug 27 01:19:32 2020 +0900
@@ -144,6 +144,14 @@
 plist0 {0} perm = []
 plist0 {suc n} perm = plist2 perm n a<sa
 
+open _=p=_
+
+←pleq  : {n  : ℕ} → (x y : Permutation n n ) → x =p= y → plist0 x ≡ plist0 y 
+←pleq {zero} x y eq = refl
+←pleq {suc n} x y eq =  ←pleq1  n a<sa where
+   ←pleq1  :   (i : ℕ ) → (i<sn : i < suc n ) →  plist2 x i i<sn ≡ plist2 y i i<sn
+   ←pleq1  zero _           = cong ( λ k → toℕ k ∷ [] ) ( peq eq (fromℕ< {zero} (s≤s z≤n)))
+   ←pleq1  (suc i) (s≤s lt) = cong₂ ( λ j k → toℕ j ∷ k ) ( peq eq (fromℕ< (s≤s lt)))  ( ←pleq1  i (<-trans lt a<sa) )
 
 headeq : {A : Set } →  {x y : A } → {xt yt : List A } → (x ∷ xt)  ≡ (y ∷ yt)  →  x ≡ y
 headeq refl = refl