From: Ferruccio Guidi 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. *)