partial update in delayed_updating

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

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 cefb45d49c977fd1f4fb7989ebc9fd32fd64a8fa..bf6831e80356072b6397c902a13803ee6610d791 100644 (file)
--- 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.