# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1376902972 -32400
# Node ID 2246a7d67ba31adfe6e1b3b42204c484c3bb036e
# Parent  a4200348a33db51f5cbf0f0e291b0dac8b8c5fe5
two yellow remain...

diff -r a4200348a33d -r 2246a7d67ba3 free-monoid.agda
--- a/free-monoid.agda	Mon Aug 19 15:44:37 2013 +0900
+++ b/free-monoid.agda	Mon Aug 19 18:02:52 2013 +0900
@@ -256,6 +256,14 @@
                                 (morph g) ( x :: xs )
                              ∎   where
                          lemma-ext3 :  ∀{ x : a } -> (morph ( solution a b f)) (x :: [])  ≡ (morph g) ( x :: []  )
-                         lemma-ext3 {x} = lemma-ext2 { x :: [] }
+                         lemma-ext3 {x} = let open ≡-Reasoning in
+                             begin
+                               (morph ( solution a b f)) (x :: [])
+                             ≡⟨  ( proj₂  ( IsMonoid.identity ( isMonoid b) )(f x) ) ⟩
+                                f x
+                             ≡⟨  sym ( ≡-cong (\f -> f x )  eq  ) ⟩
+                               (morph g) ( x :: []  )
+                             ∎   
+