...

diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index c159be66a6633198187c9ee9cd5ae79ed888b131..b66f4d457e9a12ed8dcc2ef1b732541467509048 100644 (file)
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -29,6 +29,8 @@ for @{ eq_rel ? (eq0 ?) $a $b }.
 interpretation "setoid symmetry" 'invert r = (sym ???? r).
 notation ".= r" with precedence 50 for @{'trans $r}.
 interpretation "trans" 'trans r = (trans ????? r).
+notation > ".=_0 r" with precedence 50 for @{'trans_x0 $r}.
+interpretation "trans_x0" 'trans_x0 r = (trans ????? r).
 
 nrecord unary_morphism (A,B: setoid) : Type[0] ≝
  { fun1:1> A → B;
@@ -40,6 +42,9 @@ notation "l ‡ r" with precedence 90 for @{'prop2 $l $r }.
 notation "#" with precedence 90 for @{'refl}.
 interpretation "prop1" 'prop1 c  = (prop1 ????? c).
 interpretation "refl" 'refl = (refl ???).
+notation "┼_0 c" with precedence 89 for @{'prop1_x0 $c }.
+notation "l ╪_0 r" with precedence 89 for @{'prop2_x0 $l $r }.
+interpretation "prop1_x0" 'prop1_x0 c  = (prop1 ????? c).
 
 ndefinition unary_morph_setoid : setoid → setoid → setoid.
 #S1; #S2; @ (unary_morphism S1 S2); @;
@@ -56,6 +61,7 @@ unification hint 0 ≔ o1,o2 ;
      carr X ≡ unary_morphism o1 o2.
 
 interpretation "prop2" 'prop2 l r = (prop1 ? (unary_morph_setoid ??) ? ?? l ?? r).
+interpretation "prop2_x0" 'prop2_x0 l r = (prop1 ? (unary_morph_setoid ??) ? ?? l ?? r).
 
 nlemma unary_morph_eq: ∀A,B.∀f,g: unary_morphism A B. (∀x. f x = g x) → f=g.
 #A B f g H x1 x2 E; napply (.= †E); napply H; nqed.

diff --git a/helm/software/matita/nlibrary/sets/setoids1.ma b/helm/software/matita/nlibrary/sets/setoids1.ma
index 4aac43e448e107e9559a528938d113a2a8c96443..fb960c1db0b7599af5ca9e4417b7fe08a027ba59 100644 (file)
--- a/helm/software/matita/nlibrary/sets/setoids1.ma
+++ b/helm/software/matita/nlibrary/sets/setoids1.ma
@@ -48,15 +48,19 @@ for @{ eq_rel1 ? (eq1 ?) $a $b }.
 interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r).
 interpretation "setoid symmetry" 'invert r = (sym ???? r).
 notation ".= r" with precedence 50 for @{'trans $r}.
+notation ".=_1 r" with precedence 50 for @{'trans_x1 $r}.
 interpretation "trans1" 'trans r = (trans1 ????? r).
 interpretation "trans" 'trans r = (trans ????? r).
+interpretation "trans1_x1" 'trans_x1 r = (trans1 ????? r).
 
 nrecord unary_morphism1 (A,B: setoid1) : Type[1] ≝
  { fun11:1> A → B;
    prop11: ∀a,a'. eq1 ? a a' → eq1 ? (fun11 a) (fun11 a')
  }.
-
+ 
+notation "┼_1 c" with precedence 89 for @{'prop1_x1 $c }.
 interpretation "prop11" 'prop1 c = (prop11 ????? c).
+interpretation "prop11_x1" 'prop1_x1 c = (prop11 ????? c).
 interpretation "refl1" 'refl = (refl1 ???).
 
 ndefinition unary_morphism1_setoid1: setoid1 → setoid1 → setoid1.
@@ -71,8 +75,10 @@ unification hint 0 ≔ S, T ;
  R ≟ (unary_morphism1_setoid1 S T)
 (* --------------------------------- *) ⊢
    carr1 R ≡ unary_morphism1 S T.
-
+   
+notation "l ╪_1 r" with precedence 89 for @{'prop2_x1 $l $r }.
 interpretation "prop21" 'prop2 l r = (prop11 ? (unary_morphism1_setoid1 ??) ? ?? l ?? r).
+interpretation "prop21_x1" 'prop2_x1 l r = (prop11 ? (unary_morphism1_setoid1 ??) ? ?? l ?? r).
 
 nlemma unary_morph1_eq1: ∀A,B.∀f,g: unary_morphism1 A B. (∀x. f x = g x) → f=g.
 /3/. nqed.