X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda%2Fdelifting_substitution.ma;h=344ad849021c3fc088440dc7c2b7fcc308870621;hb=8730061377260fd9d86f77b46635038e3c1411cc;hp=6e648c9a890969adb44c14ad433b247986d174a6;hpb=d5da44537d93ee16e1f440e5ce3fd69b32c3b730;p=helm.git

diff --git a/matita/matita/contribs/lambda/delifting_substitution.ma b/matita/matita/contribs/lambda/delifting_substitution.ma
index 6e648c9a8..344ad8490 100644
--- a/matita/matita/contribs/lambda/delifting_substitution.ma
+++ b/matita/matita/contribs/lambda/delifting_substitution.ma
@@ -27,12 +27,12 @@ interpretation "delifting substitution"
    'DSubst C d M = (dsubst C d M).
 
 (* Note: the notation with "/" does not work *)
-notation "hvbox( [ d ⬐ break C ] break term 55 M )"
-   non associative with precedence 55
+notation "hvbox( [ term 46 d ⬐ break term 46 C ] break term 46 M )"
+   non associative with precedence 46
    for @{ 'DSubst $C $d $M }.
 
-notation > "hvbox( [ ⬐ C ] break term 55 M )"
-   non associative with precedence 55
+notation > "hvbox( [ ⬐ term 46 C ] break term 46 M )"
+   non associative with precedence 46
    for @{ 'DSubst $C 0 $M }.
 
 lemma dsubst_vref_lt: ∀i,d,C. i < d → [d ⬐ C] #i = #i.