X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fgrammar%2Flenv_weight.ma;h=d277ed00eafb8647a8ff8c9e31653f58d48674d6;hb=439b6ec33d749ba4e6ae0938e973a85bc23e306e;hp=48ef29453580c3c168a8bcbe60d981de54056a0f;hpb=a2144f09d1bd7022c1f2dfd4909a1fb9772c8d56;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma
index 48ef29453..d277ed00e 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma
@@ -19,20 +19,20 @@ include "basic_2/grammar/lenv.ma".
 
 let rec lw L ≝ match L with
 [ LAtom       ⇒ 0
-| LPair L _ V ⇒ lw L + #[V]
+| LPair L _ V ⇒ lw L + #{V}
 ].
 
 interpretation "weight (local environment)" 'Weight L = (lw L).
 
 (* Basic properties *********************************************************)
 
-lemma lw_pair: ∀I,L,V. #[L] < #[(L.ⓑ{I}V)].
+lemma lw_pair: ∀I,L,V. #{L} < #{(L.ⓑ{I}V)}.
 /3 width=1/ qed.
 
 (* Basic eliminators ********************************************************)
 
 axiom lw_wf_ind: ∀R:predicate lenv.
-                 (∀L2. (∀L1. #[L1] < #[L2] → R L1) → R L2) →
+                 (∀L2. (∀L1. #{L1} < #{L2} → R L1) → R L2) →
                  ∀L. R L.
 
 (* Basic_1: removed theorems 2: clt_cong clt_head clt_thead *)