X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ftr_pap_tls.ma;h=da8ea1519527fc2299f606b796ea0a4ae5b1496c;hb=b1c5b3370653db6e495bbf6b3799cba592746cdd;hp=678792ff543c447bcec1b8442471e27a9254821c;hpb=0818b903bf0fb363fab2d7d9f1da64956ea54e81;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
index 678792ff5..da8ea1519 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
@@ -20,7 +20,7 @@ include "ground/lib/stream_tls.ma".
 (* Constructions with stream_tls ********************************************)
 
 lemma tr_pap_plus (p1) (p2) (f):
-      (⇂*[ninj p2]f)@❨p1❩+f@❨p2❩ = f@❨p1+p2❩.
+      (⇂*[ninj p2]f)＠⧣❨p1❩+f＠⧣❨p2❩ = f＠⧣❨p1+p2❩.
 #p1 #p2 elim p2 -p2
 [ * #p #f //
 | #i #IH * #p #f