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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pat.ma
index 90dd95a77..6e5d0c6e6 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pat.ma
@@ -21,7 +21,7 @@ include "ground/relocation/tr_pap.ma".
 (* Constructions with pr_pat ***********************************************)
 
 (*** at_total *)
-lemma tr_pat_total: ∀i1,f. @❨i1,𝐭❨f❩❩ ≘ f@❨i1❩.
+lemma tr_pat_total: ∀i1,f. ＠⧣❨i1,𝐭❨f❩❩ ≘ f＠⧣❨i1❩.
 #i1 elim i1 -i1
 [ * // | #i #IH * /3 width=1 by tr_pat_succ_sn/ ]
 qed.
@@ -30,5 +30,5 @@ qed.
 
 (*** at_inv_total *)
 lemma tr_pat_inv_total (f):
-      ∀i1,i2. @❨i1, 𝐭❨f❩❩ ≘ i2 → f@❨i1❩ = i2.
+      ∀i1,i2. ＠⧣❨i1, 𝐭❨f❩❩ ≘ i2 → f＠⧣❨i1❩ = i2.
 /2 width=6 by pr_pat_mono/ qed-.