X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fcontribs%2FPREDICATIVE-TOPOLOGY%2Fac_defs.ma;h=d23ed4e1a4272d26fb6dc8b62e67f4c593ad9f35;hb=07151480b04db0ef4e77d09a5b7559ae5ab25ab4;hp=f2cd4860fb95effe7b5f054cad9362f56a27c769;hpb=a6378eaf623f898f8cbea4381a1ea7132146c8c2;p=helm.git

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
index f2cd4860f..d23ed4e1a 100644
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
@@ -30,7 +30,7 @@ set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/ac_defs".
      of the aceq predicate given inside the category. Then we prove the 
      properties of the equality that usually are axiomatized inside the 
      category structure. This makes categories easier to use
-*) 
+     *) 
 
 record AC: Type \def {
    ac: Type;
@@ -40,5 +40,6 @@ record AC: Type \def {
 
 coercion ac. 
 
-inductive eq (A:AC) : A \to A \to Prop \def
-   | eq_refl: \forall a. acin ? a \to eq A a a.
+inductive eq (A:AC) (a:A): A \to Prop \def
+   | eq_refl:   acin ? a \to eq A a a.
+(*   | eq_sing_r: \forall b,c. eq A a b \to aceq A b c \to eq A a c. *)