--- a/Solvable.agda	Mon Aug 17 15:12:17 2020 +0900
+++ b/Solvable.agda	Mon Aug 17 15:12:36 2020 +0900
@@ -95,38 +95,6 @@
        mpf p (mpf q (mpf r ε))
     ∎ where open EqReasoning (Algebra.Group.setoid G)
 
-mpg : {x : Carrier } → (m : MP x ) → Carrier → Carrier
-mpg {x} (am x) y = y ∙ x
-mpg (m o m₁) y = mpf m₁ ( mpf m y )
-
-mp-flatten-g : {x : Carrier } → (m : MP x ) → Carrier 
-mp-flatten-g {x} m = mpg {x} m ε 
-  
-∙-flatten-g : {x : Carrier } → (m : MP x ) → x ≈ mp-flatten-g m
-∙-flatten-g {x} (am x) = gsym (proj₁ identity _)
-∙-flatten-g {_} (am x o q) = {!!} -- ∙-cong ( ∙-flatten-g q ) grefl
-∙-flatten-g (_o_ {_} {z} (_o_ {x} {y} p q) r) = lemma9 _ _ _ {!!} ( ∙-flatten-g {z} r ) where
-   mp-cong : {p q r : Carrier} → (P : MP p)  → q ≈ r → mpg P q ≈ mpg P r
-   mp-cong (am x) q=r = {!!} -- ∙-cong grefl q=r
-   mp-cong (P o P₁) q=r = {!!} -- mp-cong P ( mp-cong P₁ q=r )
-   mp-assoc : {p q r : Carrier} → (P : MP p)  → mpg P q ∙ r ≈ mpg P (q ∙ r )
-   mp-assoc (am x) = {!!} -- assoc _ _ _ 
-   mp-assoc {p} {q} {r} (P o P₁) = begin
-       {!!}      ≈⟨ {!!} ⟩
-       {!!}
-    ∎ where open EqReasoning (Algebra.Group.setoid G)
-   lemma9 : (x y z : Carrier) →  x ∙ y ≈ mpg p (mpg q ε) → z ≈ mpg r ε →  x ∙ y ∙ z ≈ mp-flatten-g ((p o q) o r)
-   lemma9 x y z t s = begin
-       {!!}                ≈⟨ {!!}  ⟩
-       {!!}
-    ∎ where open EqReasoning (Algebra.Group.setoid G)
-
-tet1 : (f g : Carrier ) → {!!}
-tet1 f g = mp-flatten-g ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))
-
-tet2 : (f g : Carrier ) → {!!}
-tet2 f g = mp-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ )))
-
 lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹
 lemma5 f g = begin
      g ⁻¹ ∙ f ⁻¹                                     ≈⟨ gsym (proj₂ identity _) ⟩