# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1376894677 -32400
# Node ID a4200348a33db51f5cbf0f0e291b0dac8b8c5fe5
# Parent  ab186f0e7b7a426d1fa8192a722a8b35b223b6f3
fix

diff -r ab186f0e7b7a -r a4200348a33d free-monoid.agda
--- a/free-monoid.agda	Mon Aug 19 14:02:41 2013 +0900
+++ b/free-monoid.agda	Mon Aug 19 15:44:37 2013 +0900
@@ -255,7 +255,7 @@
                              ≡⟨ 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 :: [] }
+                         lemma-ext3 :  ∀{ x : a } -> (morph ( solution a b f)) (x :: [])  ≡ (morph g) ( x :: []  )
+                         lemma-ext3 {x} = lemma-ext2 { x :: [] }