X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fapps_2%2Fmodels%2Fli.ma;h=b3ad3915733a01f5e97978b1f0cd49ade8bc0292;hp=4d36f142788b2b4c4efe64aa8a6b14906bd1e828;hb=f308429a0fde273605a2330efc63268b4ac36c99;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b

diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/li.ma b/matita/matita/contribs/lambdadelta/apps_2/models/li.ma
index 4d36f1427..b3ad39157 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/models/li.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/models/li.ma
@@ -20,7 +20,7 @@ include "apps_2/notation/models/inwbrackets_4.ma".
 
 inductive li (M) (gv): relation2 lenv (evaluation M) ≝
 | li_atom: ∀lv. li M gv (⋆) lv
-| li_abbr: ∀lv,d,L,V. li M gv L lv → ⟦V⟧[gv, lv] = d → li M gv (L.ⓓV) (⫯[0←d]lv)
+| li_abbr: ∀lv,d,L,V. li M gv L lv → ⟦V⟧[gv,lv] = d → li M gv (L.ⓓV) (⫯[0←d]lv)
 | li_abst: ∀lv,d,L,W. li M gv L lv → li M gv (L.ⓛW) (⫯[0←d]lv)
 | li_unit: ∀lv,d,I,L. li M gv L lv → li M gv (L.ⓤ{I}) (⫯[0←d]lv)
 | li_veq : ∀lv1,lv2,L. li M gv L lv1 → lv1 ≗ lv2 → li M gv L lv2