X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBase-2%2Fpreamble.ma;h=f04df2037817bde872bd6cddab9cbee972994981;hb=fdda444a05fe4c68c925cd94e4e3a38c93d0c35f;hp=84a4955459323e85637bb4198731a7018e291d72;hpb=9376f52b7f5890d924ae7d93bcae2af9e516126d;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
index 84a495545..f04df2037 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Base-2/preamble.ma
@@ -16,8 +16,6 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Base-2/preamble".
 
 include "../Base-1/definitions.ma".
 
-alias id "le_ind" = "cic:/Coq/Init/Peano/le_ind.con".
-
 default "equality"
  cic:/Coq/Init/Logic/eq.ind
  cic:/matita/LAMBDA-TYPES/Base-1/preamble/sym_eq.con