X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2Fsets%2Fsets.ma;h=113654ad330de847908ae68b3fcf65faaf9c3033;hb=924e808f1bc958a2d3c8ac05c96aeb8bc1f6d791;hp=0e2dd418d3c19ef4e00d02e02c8ed15c79175734;hpb=bac3136bf99a18374b91e1ec900e455567e8f741;p=helm.git

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 0e2dd418d..113654ad3 100644
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -323,6 +323,7 @@ nlemma first_omomorphism_theorem_functions1:
  #A; #B; #f; #x; napply refl;
 nqed.
 
+alias symbol "eq" = "setoid eq".
 ndefinition surjective ≝
  λA,B.λS: ext_powerclass A.λT: ext_powerclass B.λf:unary_morphism A B.
   ∀y. y ∈ T → ∃x. x ∈ S ∧ f x = y.