X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fgrammar%2Fcl_weight.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fgrammar%2Fcl_weight.ma;h=925b84a34aca11d1ee53dda0c76ea3b92b67a2c1;hb=48b202cd4ccd3ffc10f9a134314f747fdee30d36;hp=22818a9802bf43b3292d2f6b6421ec4bd3b56403;hpb=e4328c9691fa85434acfb24eaedcb15ea2263b28;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
index 22818a980..925b84a34 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
@@ -31,7 +31,7 @@ axiom cw_wf_ind: ∀R:lenv→predicate term.
                  ∀L,T. R L T.
 
 (* Basic_1: was: flt_shift *)
-lemma cw_shift: ∀K,I,V,T. #[K. 𝕓{I} V, T] < #[K, 𝕔{I} V. T].
+lemma cw_shift: ∀K,I,V,T. #[K. ⓑ{I} V, T] < #[K, ②{I} V. T].
 normalize //
 qed.