--- a/src/Putil.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/Putil.agda	Sat Sep 16 14:59:33 2023 +0900
@@ -29,7 +29,7 @@
 -- An inductive construction of permutation
 
 pprep  : {n : ℕ }  → Permutation n n → Permutation (suc n) (suc n)
-pprep {n} perm =  permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
+pprep {n} perm =  permutation p→ p← piso←  piso→ where
    p→ : Fin (suc n) → Fin (suc n)
    p→ zero = zero
    p→ (suc x) = suc ( perm  ⟨$⟩ʳ x)
@@ -47,7 +47,7 @@
    piso→ (suc x) = cong (λ k → suc k ) (inverseˡ perm) 
 
 pswap  : {n : ℕ }  → Permutation n n → Permutation (suc (suc n)) (suc (suc  n ))
-pswap {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
+pswap {n} perm = permutation p→ p← piso←  piso→ where
    p→ : Fin (suc (suc n)) → Fin (suc (suc n)) 
    p→ zero = suc zero 
    p→ (suc zero) = zero 
@@ -127,7 +127,7 @@
 
 pins  : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n)
 pins {_} {zero} _ = pid
-pins {suc n} {suc m} (s≤s  m≤n) = permutation p← p→  record { left-inverse-of = piso← ; right-inverse-of = piso→ } where
+pins {suc n} {suc m} (s≤s  m≤n) = permutation p← p→ piso→   piso← where
 
    next : Fin (suc (suc n)) → Fin (suc (suc n))
    next zero = suc zero
@@ -467,7 +467,7 @@
 
 -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] → 0 ∷ 1 ∷ 2 ∷ [] 
 shrink : {n  : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n
-shrink {n} perm p0=0  = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
+shrink {n} perm p0=0  = permutation p→ p← piso← piso→  where
 
    p→ : Fin n → Fin n 
    p→ x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) 
@@ -496,9 +496,9 @@
           plem1 = begin
                suc t1
             ≡⟨ sym e1 ⟩
-               Inverse.to perm Π.⟨$⟩ suc t
-            ≡⟨ cong (λ k →  Inverse.to perm Π.⟨$⟩ k ) (sym e0) ⟩
-               Inverse.to perm Π.⟨$⟩ ( Inverse.from perm Π.⟨$⟩ suc x )
+               Inverse.to perm  _
+            ≡⟨ cong (λ k →  Inverse.to perm k ) (sym e0) ⟩
+               Inverse.to perm ( Inverse.from perm _ )
             ≡⟨ inverseʳ perm   ⟩
                suc x
             ∎ 
@@ -517,14 +517,11 @@
           plem2 refl = refl
           plem3 :  suc t1 ≡ suc x
           plem3 = begin
-               suc t1
-            ≡⟨ sym e1 ⟩
-               Inverse.from perm Π.⟨$⟩ suc t
-            ≡⟨ cong (λ k →  Inverse.from perm Π.⟨$⟩ k ) (sym e0 ) ⟩
-               Inverse.from perm Π.⟨$⟩ ( Inverse.to perm Π.⟨$⟩ suc x )
-            ≡⟨ inverseˡ perm   ⟩
-               suc x
-            ∎
+               suc t1 ≡⟨ sym e1 ⟩
+               Inverse.from perm (suc t)  ≡⟨ cong (λ k →  Inverse.from perm k ) (sym e0 ) ⟩
+               Inverse.from perm ((Inverse.to perm (suc x)) ) ≡⟨ cong (λ k →  Inverse.from perm (Inverse.to perm (suc x)) ) (sym e0 ) ⟩
+               Inverse.from perm ( Inverse.to perm  _ ) ≡⟨ inverseˡ perm   ⟩
+               suc x ∎
 
 shrink-iso : { n : ℕ } → {perm : Permutation n n} → shrink (pprep perm)  refl =p=  perm
 shrink-iso {n} {perm} = record { peq = λ q → refl  } 

--- a/src/Symmetric.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/Symmetric.agda	Sat Sep 16 14:59:33 2023 +0900
@@ -22,11 +22,11 @@
 
 -- Data.Fin.Permutation.id
 pid : {p : ℕ } → Permutation p p
-pid = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }
+pid = permutation fid fid (λ x → refl) (λ x → refl) -- record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl } 
 
 -- Data.Fin.Permutation.flip
 pinv : {p : ℕ } → Permutation p p → Permutation p p
-pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P }
+pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) (λ x → inverseˡ P ) ( λ x → inverseʳ P) -- record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P }
 
 record _=p=_ {p : ℕ } ( x y : Permutation p p )  : Set where
     field
@@ -57,7 +57,13 @@
 presp : { p : ℕ } {x y u v : Permutation p p } → x =p= y → u =p= v → (x ∘ₚ u) =p= (y ∘ₚ v)
 presp {p} {x} {y} {u} {v} x=y u=v = record { peq = λ q → lemma4 q } where
    lemma4 : (q : Fin p) → ((x ∘ₚ u) ⟨$⟩ʳ q) ≡ ((y ∘ₚ v) ⟨$⟩ʳ q)
-   lemma4 q = trans (cong (λ k → Inverse.to u Π.⟨$⟩ k) (peq x=y q) ) (peq u=v _ )
+   lemma4 q = begin
+          ((x ∘ₚ u) ⟨$⟩ʳ q) ≡⟨ peq u=v _ ⟩
+          ((x ∘ₚ v) ⟨$⟩ʳ q) ≡⟨ cong (λ k → Inverse.to v k  ) (peq x=y _) ⟩
+          ((y ∘ₚ v) ⟨$⟩ʳ q) ∎  
+     where 
+       open ≡-Reasoning
+   -- lemma4 q = trans (cong (λ k → Inverse.to u Π.⟨$⟩ k) (peq x=y q) ) (peq u=v _ )
 passoc : { p : ℕ } (x y z : Permutation p p) → ((x ∘ₚ y) ∘ₚ z) =p=  (x ∘ₚ (y ∘ₚ z))
 passoc x y z = record { peq = λ q → refl }
 p-inv : { p : ℕ } {i j : Permutation p p} →  i =p= j → (q : Fin p) → pinv i ⟨$⟩ʳ q ≡ pinv j ⟨$⟩ʳ q

--- a/src/sym5.agda	Sat Sep 16 13:14:17 2023 +0900
+++ b/src/sym5.agda	Sat Sep 16 14:59:33 2023 +0900
@@ -14,7 +14,7 @@
 
 open import Gutil 
 open import Putil 
-open import Solvable using (solvable)
+open import Solvable (Symmetric 5)
 open import  Relation.Binary.PropositionalEquality hiding ( [_] )
 
 open import Data.Fin hiding (_<_ ; _≤_  ; lift )
@@ -30,8 +30,9 @@
 
 open _∧_
 
-¬sym5solvable : ¬ ( solvable (Symmetric 5) )
+¬sym5solvable : ¬ solvable 
 ¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot0 (dervied-length sol) 0<3 0<4 ) ) where
+
 --
 --    dba       1320      d → b → a → d
 --    (dba)⁻¹   3021      a → b → d → a
@@ -43,7 +44,6 @@
      open ≡-Reasoning
 
      open solvable
-     open Solvable ( Symmetric 5) 
      end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x →  x =p= pid  
      end5 x der = end sol x der