definition of eq improved (?) parametrizing an argument

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
index f2cd4860fb95effe7b5f054cad9362f56a27c769..d23ed4e1a4272d26fb6dc8b62e67f4c593ad9f35 100644 (file)
--- 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. *)