X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Flift_depth.ma;h=bf6831e80356072b6397c902a13803ee6610d791;hb=36660809dcfb90bea480c84997cfb40f347e0f0c;hp=cefb45d49c977fd1f4fb7989ebc9fd32fd64a8fa;hpb=f717d9ef23433a96583a1bc8ae6b903689d5f033;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_depth.ma
index cefb45d49..bf6831e80 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_depth.ma
@@ -39,3 +39,10 @@ lemma lift_rmap_decompose (p) (f):
   ]
 ]
 qed.
+
+lemma lift_rmap_pap_le (f) (p) (n):
+      (↑[p]𝐢)@❨n❩ < ↑❘p❘ → (↑[p]𝐢)@❨n❩ = (↑[p]f)@❨n❩.
+#f #p #n #Hn
+>(tr_pap_eq_repl … (↑[p]f) … (lift_rmap_decompose …))
+<tr_compose_pap @tr_pap_pushs_le //
+qed.