update in ground

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / tr_pap_pn.ma

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma
index 96eaa241f056e7d273d31dde50d4bf36ef1e02b7..09b342d3d16c7dce2c197570434576b1a615dd9d 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma
@@ -17,10 +17,16 @@ include "ground/relocation/tr_pap.ma".
 
 (* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
 
+(* Constructions with tr_push ***********************************************)
+
+lemma tr_pap_push (f):
+      ∀i. ↑(f＠⧣❨i❩) = (⫯f)＠⧣❨↑i❩.
+// qed.
+
 (* Constructions with tr_next ***********************************************)
 
 (*** apply_S2 *)
 lemma tr_pap_next (f):
-      ∀i. ↑(f@❨i❩) = (↑f)@❨i❩.
+      ∀i. ↑(f＠⧣❨i❩) = (↑f)＠⧣❨i❩.
 * #p #f * //
 qed.