X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationsEquivalentToGeneralizedArrows.v;h=0428638e69ad226b2789d72e1347a387e385700a;hp=c8a7f723cc31aea531bc99a3f2b48a75dd90b82d;hb=e6bd3d7623740382a9af0f6d39e8304b1358d847;hpb=428a230cd3ddc9182695ddacaff9eabd67d954f7

diff --git a/src/ReificationsEquivalentToGeneralizedArrows.v b/src/ReificationsEquivalentToGeneralizedArrows.v
index c8a7f72..0428638 100644
--- a/src/ReificationsEquivalentToGeneralizedArrows.v
+++ b/src/ReificationsEquivalentToGeneralizedArrows.v
@@ -83,8 +83,4 @@ Section ReificationsEquivalentToGeneralizedArrows.
     apply (step1_niso K C (reification_from_garrow K C garrow)).
     Qed.
 
-  Theorem ReificationsAreGArrows : IsomorphicCategories CategoryOfReifications CategoryOfGeneralizedArrows.
-    admit.
-    Qed.
-
 End ReificationsEquivalentToGeneralizedArrows.