partial commit in delayed_updating

[helm.git] / matita / matita / contribs / lambdadelta / ground / relocation / tr_pap_pap.ma

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 65cb40105072455c645d23178671263486846082..03a008c9640194a3ff4ff23a6886d3ffb733f109 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pap.ma
@@ -14,9 +14,11 @@
 
 include "ground/relocation/tr_pap_pat.ma".
 
+(* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
+
 (* Main inversions **********************************************************)
 
 (*** 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-.