X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FLAMBDA-TYPES%2FLevel-1%2FBase%2Fext%2Fpreamble.ma;h=b4c69f299f366435e7fbad576a9d2c8437580691;hb=94873bb61a663b4fca3dc6d07b7bb9f42122003e;hp=040b878aa0032faecd54e3af1874aceb964bd9a5;hpb=00305d361464ea4c1c071b9be29482198d521eda;p=helm.git

diff --git a/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma b/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma
index 040b878aa..b4c69f299 100644
--- a/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma
+++ b/matita/contribs/LAMBDA-TYPES/Level-1/Base/ext/preamble.ma
@@ -152,8 +152,6 @@ theorem plus_le_reg_l: \forall p,n,m. p + n <= p + m \to n <= m.
  intros. apply plus_le_reg_l; auto.
 qed.
 
-definition sym_equal \def sym_eq.
-
 default "equality"
  cic:/Coq/Init/Logic/eq.ind
  cic:/matita/LAMBDA-TYPES/Level-1/Base/ext/preamble/sym_eq.con