Mercurial > hg > Members > kono > Proof > category

changeset 166:2246a7d67ba3

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
two yellow remain...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 19 Aug 2013 18:02:52 +0900
parents a4200348a33d
children c3863043c4a3
files free-monoid.agda
diffstat 1 files changed, 9 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- 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 :: []  )
+                             ∎   
+