- matitaInit matitaprover matitadep matitamake:

[helm.git] / matita / contribs / LAMBDA-TYPES / Base-1 / preamble.ma

diff --git a/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma b/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma
index 44823fc814b685f673bb1665b1a238e195c842c8..f5ad380c9d421adc85cbd0164c695836c0b61644 100644 (file)
--- a/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma
+++ b/matita/contribs/LAMBDA-TYPES/Base-1/preamble.ma
@@ -36,6 +36,7 @@ alias id "False_ind" = "cic:/Coq/Init/Logic/False_ind.con".
 alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)".
 alias id "land" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)".
 alias id "le" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)".
+alias id "le_ind" = "cic:/Coq/Init/Peano/le_ind.con".
 alias id "le_lt_n_Sm" = "cic:/Coq/Arith/Lt/le_lt_n_Sm.con".
 alias id "le_lt_or_eq" = "cic:/Coq/Arith/Lt/le_lt_or_eq.con".
 alias id "le_n" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)".
@@ -48,6 +49,7 @@ alias id "le_plus_l" = "cic:/Coq/Arith/Plus/le_plus_l.con".
 alias id "le_plus_minus" = "cic:/Coq/Arith/Minus/le_plus_minus.con".
 alias id "le_plus_minus_r" = "cic:/Coq/Arith/Minus/le_plus_minus_r.con".
 alias id "le_plus_r" = "cic:/Coq/Arith/Plus/le_plus_r.con".
+alias id "le_pred_n" = "cic:/Coq/Arith/Le/le_pred_n.con".
 alias id "le_S" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1/2)".
 alias id "le_S_n" = "cic:/Coq/Arith/Le/le_S_n.con".
 alias id "le_Sn_n" = "cic:/Coq/Arith/Le/le_Sn_n.con".