From b2d91e46900424ce5eb5a058c33841e72cc4b229 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 30 Dec 2009 17:30:48 +0000 Subject: [PATCH] ... --- helm/software/matita/nlibrary/sets/setoids1.ma | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma index 85038ab16..6d6b68743 100644 --- a/helm/software/matita/nlibrary/sets/setoids1.ma +++ b/helm/software/matita/nlibrary/sets/setoids1.ma @@ -14,6 +14,7 @@ include "properties/relations1.ma". include "sets/setoids.ma". +include "hints_declaration.ma". nrecord setoid1: Type[2] ≝ { carr1:> Type[1]; @@ -63,3 +64,16 @@ nrecord binary_morphism1 (A,B,C:setoid1) : Type[1] ≝ interpretation "prop11" 'prop1 c = (prop11 ????? c). interpretation "prop21" 'prop2 l r = (prop21 ???????? l r). interpretation "refl1" 'refl = (refl1 ???). + +ndefinition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1. + #s; #s1; @ (unary_morphism1 s s1); @ + [ #f; #g; napply (∀a:s. f a = g a) + | #x; #a; napply refl1 + | #x; #y; #H; #a; napply sym1; nauto + | #x; #y; #z; #H1; #H2; #a; napply trans1; ##[##2: napply H1 | ##skip | napply H2]##] +nqed. + +unification hint 0 ≔ S, T ; + R ≟ (unary_morphism1_setoid1 S T) +(* --------------------------------- *) ⊢ + carr1 R ≡ unary_morphism1 S T. \ No newline at end of file -- 2.39.2