--- a/CCC.agda	Thu Apr 18 10:00:20 2019 +0900
+++ b/CCC.agda	Thu Apr 18 20:07:22 2019 +0900
@@ -30,6 +30,7 @@
        -- closed
        e4a : {a b c : Obj A} → { h : Hom A (c ∧ b) a } →  A [ A [ ε o < A [ (h *) o π ]  ,  π' > ] ≈ h ]
        e4b : {a b c : Obj A} → { k : Hom A c (a <= b ) } →  A [ ( A [ ε o < A [ k o  π ]  ,  π' > ] ) * ≈ k ]
+       *-cong :  {a b c : Obj A} → { f f' : Hom A (a ∧ b) c } → A [ f ≈ f' ]  → A [  f *  ≈  f' * ] 
 
      e'2 : A [ ○ １ ≈ id1 A １ ]
      e'2 = let open  ≈-Reasoning A in begin