checkpoint

[coq-hetmet.git] / src / GeneralizedArrowFromReification.v

diff --git a/src/GeneralizedArrowFromReification.v b/src/GeneralizedArrowFromReification.v
index 627aa22..8bed743 100644 (file)
--- 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