From 07151480b04db0ef4e77d09a5b7559ae5ab25ab4 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 18 Oct 2005 12:16:35 +0000 Subject: [PATCH] definition of eq improved (?) parametrizing an argument --- helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) 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. *) -- 2.39.2