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
      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;
 
 record AC: Type \def {
    ac: Type;


@@ -40,5 +40,6 @@ record AC: Type \def {
 
 coercion ac. 
 
 
 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. *)