X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationsEquivalentToGeneralizedArrows.v;h=0428638e69ad226b2789d72e1347a387e385700a;hp=bb5df17fb0a5b55a99aea32e812b539509c7f18d;hb=f9297f3fba59884fe98eb4f9257a1fb7552bfd0a;hpb=7300187652058f4c24fd4527d9a5833583959fb4

diff --git a/src/ReificationsEquivalentToGeneralizedArrows.v b/src/ReificationsEquivalentToGeneralizedArrows.v
index bb5df17..0428638 100644
--- a/src/ReificationsEquivalentToGeneralizedArrows.v
+++ b/src/ReificationsEquivalentToGeneralizedArrows.v
@@ -83,9 +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.