X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fgrammar%2Flenv.ma;h=95e155b74e52d06592f6e3553eddcf402562c519;hb=e76eade57c0454a58b0d58e5484efe9af417847e;hp=a15c5309b9b3308daae7f84e35b158d67e8a9296;hpb=65008df95049eb835941ffea1aa682c9253c4c2b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
index a15c5309b..95e155b74 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv.ma
@@ -29,7 +29,7 @@ inductive lenv: Type[0] ≝
 interpretation "sort (local environment)"
    'Star = LAtom.
 
-interpretation "environment binding construction (binary)"
+interpretation "local environment binding construction (binary)"
    'DxBind2 L I T = (LPair L I T).
 
 interpretation "abbreviation (local environment)"
@@ -40,7 +40,7 @@ interpretation "abstraction (local environment)"
 
 (* Basic properties *********************************************************)
 
-axiom lenv_eq_dec: ∀L1,L2:lenv. Decidable (L1 = L2).
+axiom eq_lenv_dec: ∀L1,L2:lenv. Decidable (L1 = L2).
 
 (* Basic inversion lemmas ***************************************************)