X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ftr_pap_pn.ma;h=09b342d3d16c7dce2c197570434576b1a615dd9d;hb=77479649510792efe4d9cbff508e118360862594;hp=ce4a0aa3229524ca1dd505e53dc7840538f5bcb7;hpb=9b4e20442ec5a4028cfe2b6fe836c94acdb033b8;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 ce4a0aa32..09b342d3d 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma
@@ -20,13 +20,13 @@ include "ground/relocation/tr_pap.ma".
 (* Constructions with tr_push ***********************************************)
 
 lemma tr_pap_push (f):
-      ∀i. ↑(f@❨i❩) = (⫯f)@❨↑i❩.
+      ∀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.