X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Flift_structure.ma;h=d18f72b52d1c152285d8643c05b3a7eac40d93e2;hb=f83215ca9b8d0019c85a991ec90c6c658c0aaff8;hp=4577a65b69ea451d9719d30152e3ca4865136a12;hpb=e8571cfbc30a3da656cff0c0e0f0ee747e8c4cdd;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
index 4577a65b6..d18f72b52 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
@@ -20,7 +20,7 @@ include "delayed_updating/substitution/lift_eq.ma".
 (* Constructions with structure ********************************************)
 
 lemma lift_d_empty_dx (n) (p) (f):
-      (⊗p)◖𝗱❨(↑[p]f)@❨n❩❩ = ↑[f](p◖𝗱❨n❩).
+      (⊗p)◖𝗱((↑[p]f)@❨n❩) = ↑[f](p◖𝗱n).
 #n #p @(path_ind_lift … p) -p // [ #m #l #p |*: #p ] #IH #f
 [ <lift_rmap_d_sn <lift_path_d_lcons_sn //
 | <lift_rmap_L_sn <lift_path_L_sn <IH //