--- a/free-monoid.agda	Mon Aug 19 13:28:08 2013 +0900
+++ b/free-monoid.agda	Mon Aug 19 14:02:41 2013 +0900
@@ -227,11 +227,35 @@
              { g :  Hom B (Generator a) b } → (FMap U g) o (eta a )  ≡ f  → B [ solution a b f ≈ g ]
         uniquness {a} {b} {f} {g} eq =  
                      Extensionarity  ( lemma-ext2 ) where
-                        lemma-ext3 : (morph g) [] ≡  ε b
-                        lemma-ext3 = {!!}
                         lemma-ext2 : ( ∀{ x : List a } -> (morph ( solution a b f)) x  ≡ (morph g) x  )
                         -- (morph ( solution a b f)) []  ≡ (morph g) []  )
-                        lemma-ext2 {[]}       = trans (identity (solution a b f)) (sym lemma-ext3 )
-                        lemma-ext2 {x :: xs}  = {!!}
+                        lemma-ext2 {[]} = let open ≡-Reasoning in
+                             begin
+                                (morph ( solution a b f)) []
+                             ≡⟨ identity ( solution a b f) ⟩
+                                ε b
+                             ≡⟨ sym ( identity g ) ⟩
+                                (morph g) []
+                             ∎  
+                        lemma-ext2 {x :: xs}  = let open ≡-Reasoning in
+                             begin
+                                (morph ( solution a b f)) ( x :: xs )
+                             ≡⟨ mdistr ( solution a b f) {x :: []} {xs} ⟩
+                                 _∙_ b ((morph ( solution a b f)) ( x :: []) )  ((morph ( solution a b f)) xs )
+                             ≡⟨  ≡-cong ( \ k -> (_∙_ b ((morph ( solution a b f)) ( x :: []) ) k )) (lemma-ext2 {xs} )   ⟩
+                                 _∙_ b ((morph ( solution a b f)) ( x :: []) )  ((morph g) ( xs ))
+                             ≡⟨  ≡-cong ( \k -> ( _∙_ b ( k x ) ((morph g) ( xs )) )) (
+                                 begin
+                                     ( \x -> (morph ( solution a b f)) ( x :: [] ) )
+                                 ≡⟨ Extensionarity lemma-ext3 ⟩
+                                     ( \x -> (morph g) ( x :: [] ) )
+                                 ∎  
+                             ) ⟩
+                                 _∙_ b ((morph g) ( x :: [] )) ((morph g) ( xs ))
+                             ≡⟨ sym ( mdistr g ) ⟩
+                                (morph g) ( x :: xs )
+                             ∎   where
+                          lemma-ext3 :  ∀{ x : a } -> (morph ( solution a b f)) (x :: [])  ≡ (morph g) ( x :: []  )
+                          lemma-ext3 {x} = lemma-ext2 { x :: [] }