update in ground and static_2

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

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma
index e6134e7f9a77899840332443c91e06f67bed89d4..d15047b0c63783a7bd033af33eff400b9a832998 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma
@@ -12,33 +12,33 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/functions/droppreds_2.ma".
+include "ground/notation/functions/downspoonstar_2.ma".
 include "ground/lib/stream_tls.ma".
 include "ground/relocation/gr_tl.ma".
 
 (* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************)
 
 (*** tls *)
-definition gr_tls (n) (f:gr_map) â\89\9d â«°*[n]f.
+definition gr_tls (n) (f:gr_map) â\89\9d â\87£*[n]f.
 
 interpretation
   "iterated tail (generic relocation maps)"
-  'DropPreds n f = (gr_tls n f).
+  'DownSpoonStar n f = (gr_tls n f).
 
 (* Basic constructions (specific) *******************************************)
 
 (*** tls_O *)
-lemma gr_tls_zero (f): f = ⫱*[𝟎] f.
+lemma gr_tls_zero (f): f = â«°*[𝟎] f.
 // qed.
 
 (*** tls_swap *)
-lemma gr_tls_tl (n) (f): ⫱⫱*[n] f = ⫱*[n] ⫱f.
+lemma gr_tls_tl (n) (f): â«°â«°*[n] f = â«°*[n] â«°f.
 /2 width=1 by stream_tls_tl/ qed.
 
 (*** tls_S *)
-lemma gr_tls_succ (n) (f): ⫱⫱*[n] f = ⫱*[↑n] f.
+lemma gr_tls_succ (n) (f): â«°â«°*[n] f = â«°*[↑n] f.
 /2 width=1 by stream_tls_succ/ qed.
 
 (*** tls_xn *)
-lemma gr_tls_swap (n) (f): ⫱*[n] ⫱f = ⫱*[↑n] f.
+lemma gr_tls_swap (n) (f): â«°*[n] â«°f = â«°*[↑n] f.
 // qed.