X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Flift_rmap_closed.ma;h=cc3e61bf7c5ebcfbf3097bff72a55b87e966c070;hb=829e3a8af3229c4e625245f7265dd67939da98c4;hp=58bef8153e3ec21c96de6c4d00400402ac358b17;hpb=b1c5b3370653db6e495bbf6b3799cba592746cdd;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma
index 58bef8153..cc3e61bf7 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_closed.ma
@@ -34,3 +34,10 @@ lemma tls_lift_rmap_closed (f) (q) (n):
 #f #q #n #H0
 /2 width=1 by tls_plus_lift_rmap_closed/
 qed-.
+
+lemma tls_succ_lift_rmap_append_L_closed_dx (f) (p) (q) (n):
+      q ϵ 𝐂❨n❩ →
+      ↑[p]f ≗ ⇂*[↑n]↑[p●𝗟◗q]f.
+#f #p #q #n #Hq
+/3 width=1 by tls_lift_rmap_closed, pcc_L_sn/
+qed-.