From d93c422814484956482b1e70d90bb443eb99af21 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 29 Sep 2009 08:18:25 +0000 Subject: [PATCH] ... --- helm/software/matita/nlibrary/sets/partitions.ma | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/helm/software/matita/nlibrary/sets/partitions.ma b/helm/software/matita/nlibrary/sets/partitions.ma index c1092c497..1dce8d535 100644 --- a/helm/software/matita/nlibrary/sets/partitions.ma +++ b/helm/software/matita/nlibrary/sets/partitions.ma @@ -26,6 +26,7 @@ alias symbol "eq" = "setoid eq". alias symbol "eq" = "setoid1 eq". alias symbol "eq" = "setoid eq". alias symbol "eq" = "setoid1 eq". +alias symbol "eq" = "setoid eq". nrecord partition (A: setoid) : Type[1] ≝ { support: setoid; indexes: qpowerclass support; @@ -175,7 +176,8 @@ napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##] nlapply(disjoint … P (f i1) (f i1') ???) [##2,3: napply f_closed; nassumption |##1: @ (fi i1 i2); @; - ##[ napply f_closed; nassumption ##| napply (. E‡#); + ##[ napply f_closed; nassumption ##| alias symbol "refl" = "refl1". +napply (. E‡#); nwhd; napply f_closed; nassumption]##] #E'; ncut(i1 = i1'); ##[ napply (f_inj … E'); nassumption; ##] #E''; nrewrite < E''; @; -- 2.39.2