X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Flift.ma;h=bfb66f1bc911e23f4b6a2b445f62fe236f6552c4;hb=e0c91d8a4422da0b39aca790e5826dc8a617b303;hp=f2b004a1898f8f7033e93e604555ee5d38af5a6c;hpb=ad49f5895fadff5a1d9845debb1c852a1455c6c9;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
index f2b004a18..bfb66f1bc 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
@@ -146,6 +146,10 @@ qed.
 
 (* Advanced constructions with proj_rmap and path_rcons *********************)
 
+lemma lift_rmap_d_dx (f) (p) (n):
+      (↑[p]f)∘𝐮❨ninj n❩ = ↑[p◖𝗱n]f.
+// qed.
+
 lemma lift_rmap_m_dx (f) (p):
       ↑[p]f = ↑[p◖𝗺]f.
 // qed.