eq -> eq0 renaming

[helm.git] / helm / software / matita / nlibrary / sets / sets.ma

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 780dc2b4caa7524493c75c78bc0db9a331171246..9fd5b7eeb77c78d77de0fb5b220f42e93f84779d 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -52,8 +52,8 @@ ndefinition seteq: ∀A. equivalence_relation1 (Ω^A).
  #A; @
   [ napply (λS,S'. S ⊆ S' ∧ S' ⊆ S)
   | /2/
-  | #S; #S'; *; /2/
-  | #S; #T; #U; *; #H1; #H2; *; /3/]
+  | #S; #S'; *; /3/
+  | #S; #T; #U; *; #H1; #H2; *; /4/]
 nqed.
 
 include "sets/setoids1.ma".
@@ -84,7 +84,7 @@ nrecord ext_powerclass (A: setoid) : Type[1] ≝
 notation > "𝛀 ^ term 90 A" non associative with precedence 70 
 for @{ 'ext_powerclass $A }.
 
-notation "Ω term 90 A \atop ≈" non associative with precedence 70 
+notation < "Ω term 90 A \atop ≈" non associative with precedence 90 
 for @{ 'ext_powerclass $A }.
 
 interpretation "extensional powerclass" 'ext_powerclass a = (ext_powerclass a).
@@ -140,12 +140,12 @@ unification hint 0 ≔  A:setoid, x, S;
 nlemma subseteq_is_morph: ∀A. unary_morphism1 (ext_powerclass_setoid A)
  (unary_morphism1_setoid1 (ext_powerclass_setoid A) CPROP).
  #A; napply (mk_binary_morphism1 … (λS,S':𝛀^A. S ⊆ S'));
- #a; #a'; #b; #b'; *; #H1; #H2; *; /4/.
+ #a; #a'; #b; #b'; *; #H1; #H2; *; /5/ by mk_iff, sym1, subseteq_trans;
 nqed.
 
 unification hint 0 ≔ A,a,a'
  (*-----------------------------------------------------------------*) ⊢
-  eq_rel ? (eq A) a a' ≡ eq_rel1 ? (eq1 (setoid1_of_setoid A)) a a'.
+  eq_rel ? (eq0 A) a a' ≡ eq_rel1 ? (eq1 (setoid1_of_setoid A)) a a'.
 
 nlemma intersect_is_ext: ∀A. 𝛀^A → 𝛀^A → 𝛀^A.
  #A; #S; #S'; @ (S ∩ S');
@@ -262,7 +262,7 @@ nqed.
 
 ndefinition image: ∀A,B. (carr A → carr B) → Ω^A → Ω^B ≝
  λA,B:setoid.λf:carr A → carr B.λSa:Ω^A.
-  {y | ∃x. x ∈ Sa ∧ eq_rel (carr B) (eq B) (f x) y}.
+  {y | ∃x. x ∈ Sa ∧ eq_rel (carr B) (eq0 B) (f x) y}.
 
 ndefinition counter_image: ∀A,B. (carr A → carr B) → Ω^B → Ω^A ≝
  λA,B,f,Sb. {x | ∃y. y ∈ Sb ∧ f x = y}.