update in delayed_updating

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

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
index f2b004a1898f8f7033e93e604555ee5d38af5a6c..bfb66f1bc911e23f4b6a2b445f62fe236f6552c4 100644 (file)
--- 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.