X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ftr_pap_pap.ma;h=03a008c9640194a3ff4ff23a6886d3ffb733f109;hb=61bc42e04598a9f5e489c3867af72e700c7fda04;hp=c3cacbbd493457421174fc3d189b578489dff511;hpb=775ab35f714568dfcd672f0dd53a00e1ba7382cd;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pap.ma
index c3cacbbd4..03a008c96 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pap.ma
@@ -20,5 +20,5 @@ include "ground/relocation/tr_pap_pat.ma".
 
 (*** apply_inj *)
 theorem tr_pap_inj (f):
-        ∀i1,i2,j. f@❨i1❩ = j → f@❨i2❩ = j → i1 = i2.
+        ∀i1,i2,j. f＠⧣❨i1❩ = j → f＠⧣❨i2❩ = j → i1 = i2.
 /2 width=4 by pr_pat_inj/ qed-.