X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ftr_compose_tls.ma;h=7d678a7f304117e6fc996f224a1fe8bc8f9967da;hb=61bc42e04598a9f5e489c3867af72e700c7fda04;hp=2ff52deecfe9f57e9bbb3184979986894b95c460;hpb=f717d9ef23433a96583a1bc8ae6b903689d5f033;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
index 2ff52deec..7d678a7f3 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
@@ -22,7 +22,7 @@ include "ground/arith/nat_rplus_pplus.ma".
 (* Advanced constructions with stream_tls ***********************************)
 
 lemma tr_compose_tls (p) (f1) (f2):
-      (⇂*[f1@❨p❩]f2)∘(⇂*[p]f1) = ⇂*[p](f2∘f1).
+      (⇂*[f1＠⧣❨p❩]f2)∘(⇂*[p]f1) = ⇂*[p](f2∘f1).
 #p elim p -p [| #p #IH ] * #q1 #f1 #f2 //
 <tr_compose_unfold <tr_pap_succ
 >nsucc_inj <stream_tls_succ_lcons <stream_tls_succ_lcons