X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ftr_id_pap.ma;h=2deb5bfa04b06f2a80aaeb70fa2bd8baa916627e;hb=77479649510792efe4d9cbff508e118360862594;hp=9a406ba8c920086e8e963d86bd823c4e6cec6825;hpb=9b4e20442ec5a4028cfe2b6fe836c94acdb033b8;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
index 9a406ba8c..2deb5bfa0 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
@@ -20,7 +20,7 @@ include "ground/relocation/tr_id_pushs.ma".
 (* Coonstructions with tr_pap ***********************************************)
 
 lemma tr_id_pap (p):
-      p = 𝐢@❨p❩.
+      p = 𝐢＠⧣❨p❩.
 #p >(tr_pushs_id p)
 /2 width=1 by tr_pap_pushs_le/
 qed.