From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 23 Oct 2009 07:20:59 +0000 (+0000)
Subject: Alias required now ??
X-Git-Tag: make_still_working~3259
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3f4b58f8e03c8cf0a40ebeaaee98e733a54ac51d;p=helm.git

Alias required now ??
---

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.