# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1586630090 -32400
# Node ID 1c659deb22f829ae8b0b46b5b908e09c8e87b0d5
# Parent  a502754b890af8e644059195aa58b0b1c1312022
loop

diff -r a502754b890a -r 1c659deb22f8 CCCGraph1.agda
--- a/CCCGraph1.agda	Sun Apr 12 03:26:35 2020 +0900
+++ b/CCCGraph1.agda	Sun Apr 12 03:34:50 2020 +0900
@@ -295,6 +295,12 @@
                   cong₂ (λ j k → < j , k > ) ( d-eval f g ) ( d-eval f₁ g ))
               d-eval (iv x (iv f f₁)) g = begin
                     eval (iv x (iv f f₁) ・ g)
+                ≡⟨⟩
+                    eval (iv x (iv f f₁ ・ g))
+                ≡⟨ {!!} ⟩
+                    eval (iv x (eval (iv f f₁ ・ g)))
+                ≡⟨ {!!} ⟩
+                    eval (iv x (eval (iv f f₁) ・ eval g))
                 ≡⟨ {!!} ⟩
                     eval (eval (iv x (iv f f₁)) ・ eval g)
                 ∎  where open ≡-Reasoning