X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fxap.ma;h=0f367b218935fe30bb24078908b49b3e678c10d5;hb=b0c6bbd5db69489a5ebd1b36de6685fa6de441b3;hp=073ffed7f560ae726941a9a370d576d02d81381d;hpb=afb5d82d388986bbeb17a4f114aebbaafc948f93;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
index 073ffed7f..0f367b218 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/xap.ma
@@ -1,20 +1,19 @@
-
 (**) (* reverse include *)
 include "ground/arith/nat_rplus_pplus.ma".
 include "ground/relocation/tr_pn_eq.ma".
 include "ground/relocation/tr_compose_pn.ma".
 include "ground/relocation/nap.ma".
-include "ground/notation/functions/apply_2.ma".
+include "ground/notation/functions/at_2.ma".
 
 definition tr_xap (f) (l:nat): nat ≝
-           (⫯f)@↑❨l❩.
+           (⫯f)＠§❨l❩.
 
 interpretation
   "functional extended application (total relocation maps)"
-  'Apply f l = (tr_xap f l).
+  'At f l = (tr_xap f l).
 
 lemma tr_xap_unfold (f) (l):
-      (⫯f)@↑❨l❩ = f＠❨l❩.
+      (⫯f)＠§❨l❩ = f＠❨l❩.
 // qed.
 
 lemma tr_xap_zero (f):
@@ -26,7 +25,7 @@ lemma tr_xap_ninj (f) (p):
 // qed.
 
 lemma tr_xap_succ_nap (f) (n):
-      ↑(f@↑❨n❩) = f＠❨↑n❩.
+      ↑(f＠§❨n❩) = f＠❨↑n❩.
 #f #n
 <tr_xap_ninj //
 qed.
@@ -78,3 +77,8 @@ theorem tr_xap_eq_repl (i):
 <tr_xap_unfold <tr_xap_unfold
 /3 width=1 by tr_push_eq_repl, tr_nap_eq_repl/
 qed.
+
+lemma tr_nap_plus (f) (m) (n):
+      ⇂*[↑n]f＠❨m❩+f＠§❨n❩ = f＠§❨m+n❩.
+/2 width=1 by eq_inv_nsucc_bi/
+qed.