X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2Flref_map_defs.ma;h=572618808d33101ac9bbcd6e1de7c45c533009e8;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=f2994f9b79b5185b4250e5ff11bc5956b703fbf0;hpb=2ff23d9306837c14c9d1a3b935a66bc71ffe87c3;p=helm.git

diff --git a/helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma b/helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma
index f2994f9b7..572618808 100644
--- a/helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma
+++ b/helm/matita/contribs/LAMBDA-TYPES/lref_map_defs.ma
@@ -18,5 +18,5 @@ include "terms_defs.ma".
 
 inductive tlref_map (A: Set) (N: Set) (map: nat \to nat): nat \to (T A N) \to (T A N) \to Prop \def
    | tlref_map_sort: \forall i. \forall k. \forall y. (tlref_map A N map i (TSort A N y k) (TSort A N y k))
-   | tlref_map_lref_lt: \forall j. \forall i. \forall y. (lt j i) \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y j))
-   | tlref_map_lref_ge: \forall j. \forall i. \forall y. (le i j) \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y (map j))).
\ No newline at end of file
+   | tlref_map_lref_lt: \forall j. \forall i. \forall y. j < i \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y j))
+   | tlref_map_lref_ge: \forall j. \forall i. \forall y. i \le j \to (tlref_map A N map i (TLRef A N y j) (TLRef A N y (map j))).