From 3f4b58f8e03c8cf0a40ebeaaee98e733a54ac51d Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 23 Oct 2009 07:20:59 +0000
Subject: [PATCH] Alias required now ??

---
 helm/software/matita/nlibrary/sets/sets.ma | 1 +
 1 file changed, 1 insertion(+)

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.
-- 
2.39.5