X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FGeneralizedArrowFromReification.v;h=8bed7436fd36363c1d0e4298d90a9c73f25e0f44;hp=627aa223e52c092396bf0652ebe9fcfa3b7e7b50;hb=be2a24c17877b3401c3c46bee1436b8ec0bbdaf5;hpb=9444d329585e0dc3400a3bbb8155900f9ad62b92

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index 627aa22..8bed743 100644
--- a/src/GeneralizedArrowFromReification.v
+++ b/src/GeneralizedArrowFromReification.v
@@ -124,6 +124,7 @@ Section GArrowFromReification.
 
   Lemma garrow_functor_monoidal_niso
     : (garrow_functor **** garrow_functor) >>>> (mon_f C) <~~~> (mon_f (enr_v_mon K)) >>>> garrow_functor.
+    unfold garrow_functor.
     admit.
     Defined.
   Lemma garrow_functor_monoidal_iso