From 28da21926eb9cab187ba8a64999c760083f60369 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jul 2009 22:43:16 +0000 Subject: [PATCH] eq moved to CProp In Prop a unification problem was not solved, but I suspect that that was a bug... --- helm/software/matita/nlibrary/algebra/magmas.ma | 3 ++- helm/software/matita/nlibrary/logic/equality.ma | 4 ++-- 2 files changed, 4 insertions(+), 3 deletions(-) diff --git a/helm/software/matita/nlibrary/algebra/magmas.ma b/helm/software/matita/nlibrary/algebra/magmas.ma index 0d4d7d6b1..28b3795c8 100644 --- a/helm/software/matita/nlibrary/algebra/magmas.ma +++ b/helm/software/matita/nlibrary/algebra/magmas.ma @@ -71,5 +71,6 @@ ndefinition mm_image: | #x; #y; *; #x0; #Hx0; *; #y0; #Hy0; nwhd; napply (ex_intro ????) [ napply (op ? x0 y0) - | nelim daemon ]##] + | napply (conj ????); + nelim daemon ]##] nqed. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma index d940b97c0..ff8cc5a13 100644 --- a/helm/software/matita/nlibrary/logic/equality.ma +++ b/helm/software/matita/nlibrary/logic/equality.ma @@ -14,9 +14,9 @@ include "logic/connectives.ma". -ninductive eq (A: Type) (a: A) : A → Prop ≝ +ninductive eq (A: Type) (a: A) : A → CProp ≝ refl: eq A a a. interpretation "leibnitz's equality" 'eq t x y = (eq t x y). -interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)). \ No newline at end of file +interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)). -- 2.39.2