update in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / delayed_updating / substitution / lift_structure.ma

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 903026e4dfd7167948257aa023b5274cf44a8ec3..4577a65b69ea451d9719d30152e3ca4865136a12 100644 (file)
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
@@ -20,9 +20,9 @@ include "delayed_updating/substitution/lift_eq.ma".
 (* Constructions with structure ********************************************)
 
 lemma lift_d_empty_dx (n) (p) (f):
-      (⊗p)◖𝗱❨(↑[p◖𝗱❨n❩]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_lcons_sn <lift_path_d_lcons_sn //
+[ <lift_rmap_d_sn <lift_path_d_lcons_sn //
 | <lift_rmap_L_sn <lift_path_L_sn <IH //
 | <lift_rmap_A_sn <lift_path_A_sn <IH //
 | <lift_rmap_S_sn <lift_path_S_sn <IH //