# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1413608673 -32400
# Node ID 0bc402f970b3466910aecc0d16693d7e5d7b80d3
# Parent  71906644d20647c029b3f54a6637375b240cf587
Proof Monad-law 1

diff -r 71906644d206 -r 0bc402f970b3 agda/similar.agda
--- a/agda/similar.agda	Sat Oct 18 13:52:18 2014 +0900
+++ b/agda/similar.agda	Sat Oct 18 14:04:33 2014 +0900
@@ -25,14 +25,15 @@
 returnSS : {A : Set} -> A -> A -> Similar A
 returnSS x y = similar [[ (show x) ]] x [[ (show y) ]] y
 
+
 --monad-law-1 : mu ∙ (fmap mu) ≡ mu ∙ mu
-
-
 monad-law-1 : {l : Level} {A : Set l} -> (s : Similar (Similar (Similar A))) -> ((mu ∙ (fmap mu)) s) ≡ ((mu ∙ mu) s)
 monad-law-1 (similar lx (similar llx (similar lllx x _ _) _ (similar _ _ _ _)) 
                      ly (similar   _ (similar _ _ _ _)  lly (similar _ _  llly y))) = begin
     similar (lx ++ (llx ++ lllx)) x (ly ++ (lly ++ llly)) y
-  ≡⟨ {!!} ⟩
+  ≡⟨ cong (\left-list -> similar left-list x (ly ++ (lly ++ llly)) y) (list-associative lx llx lllx) ⟩
+    similar (lx ++ llx ++ lllx) x (ly ++ (lly ++ llly)) y
+  ≡⟨ cong (\right-list -> similar (lx ++ llx ++ lllx) x right-list y ) (list-associative ly lly llly) ⟩
     similar (lx ++ llx ++ lllx) x (ly ++ lly ++ llly) y
   ∎