From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 18 Oct 2005 12:16:35 +0000 (+0000)
Subject: definition of eq improved (?) parametrizing an argument
X-Git-Tag: V_0_7_2_3~209
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=07151480b04db0ef4e77d09a5b7559ae5ab25ab4;p=helm.git

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 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. *)