X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ftr_pap_pn.ma;h=ce4a0aa3229524ca1dd505e53dc7840538f5bcb7;hb=775ab35f714568dfcd672f0dd53a00e1ba7382cd;hp=96eaa241f056e7d273d31dde50d4bf36ef1e02b7;hpb=56092257aa4be8e6d0ae37ee6590f6d3258b0485;p=helm.git

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 96eaa241f..ce4a0aa32 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma
@@ -17,6 +17,12 @@ 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 *)