From dc605ae41c39773f55381f241b1ed3db4acf5edd Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 29 Jun 2021 18:31:37 +0200
Subject: [PATCH] update in ground and static_2

+ notation update for tail function
+ predefined virtuals: one symbol added
---
 .../contribs/lambdadelta/apps_2/web/apps_2_src.tbl |  2 +-
 .../contribs/lambdadelta/ground/lib/stream_hdtl.ma |  8 ++++----
 .../contribs/lambdadelta/ground/lib/stream_tls.ma  | 12 ++++++------
 .../lambdadelta/ground/lib/stream_tls_eq.ma        |  2 +-
 .../{downspoon_2.ma => downdashedarrow_2.ma}       | 12 ++++++------
 ...downspoonstar_3.ma => downdashedarrowstar_3.ma} | 12 ++++++------
 .../functions/{droppred_1.ma => downspoon_1.ma}    |  4 ++--
 .../{droppreds_2.ma => downspoonstar_2.ma}         |  4 ++--
 .../ground/relocation/gr_after_after_ist.ma        |  2 +-
 .../ground/relocation/gr_after_nat_uni_tls.ma      |  4 ++--
 .../ground/relocation/gr_after_pat_tls.ma          |  2 +-
 .../ground/relocation/gr_after_pat_uni_tls.ma      |  4 ++--
 .../lambdadelta/ground/relocation/gr_coafter.ma    |  8 ++++----
 .../ground/relocation/gr_coafter_coafter_ist.ma    |  2 +-
 .../ground/relocation/gr_coafter_nat_tls.ma        |  4 ++--
 .../ground/relocation/gr_coafter_nat_tls_pushs.ma  |  2 +-
 .../ground/relocation/gr_coafter_pat_tls.ma        |  6 +++---
 .../lambdadelta/ground/relocation/gr_isd_tl.ma     |  2 +-
 .../lambdadelta/ground/relocation/gr_isd_tls.ma    |  2 +-
 .../lambdadelta/ground/relocation/gr_isf_tl.ma     |  4 ++--
 .../lambdadelta/ground/relocation/gr_isf_tls.ma    |  4 ++--
 .../lambdadelta/ground/relocation/gr_isi_tl.ma     |  2 +-
 .../lambdadelta/ground/relocation/gr_isi_tls.ma    |  2 +-
 .../lambdadelta/ground/relocation/gr_ist.ma        |  2 +-
 .../lambdadelta/ground/relocation/gr_ist_tls.ma    |  2 +-
 .../lambdadelta/ground/relocation/gr_isu_tl.ma     |  2 +-
 .../lambdadelta/ground/relocation/gr_pat_lt.ma     |  2 +-
 .../lambdadelta/ground/relocation/gr_pat_tls.ma    |  8 ++++----
 .../lambdadelta/ground/relocation/gr_sle.ma        | 10 +++++-----
 .../lambdadelta/ground/relocation/gr_sle_tls.ma    |  2 +-
 .../lambdadelta/ground/relocation/gr_sor.ma        | 14 +++++++-------
 .../lambdadelta/ground/relocation/gr_sor_tls.ma    |  2 +-
 .../lambdadelta/ground/relocation/gr_tl.ma         | 12 ++++++------
 .../lambdadelta/ground/relocation/gr_tl_eq.ma      | 14 +++++++-------
 .../lambdadelta/ground/relocation/gr_tls.ma        | 14 +++++++-------
 .../lambdadelta/ground/relocation/gr_tls_eq.ma     |  2 +-
 .../ground/relocation/gr_tls_nexts_eq.ma           |  4 ++--
 .../lambdadelta/ground/relocation/gr_tls_pushs.ma  |  2 +-
 .../ground/relocation/gr_tls_pushs_eq.ma           |  4 ++--
 .../contribs/lambdadelta/ground/web/ground_src.tbl |  8 ++++----
 .../lambdadelta/static_2/relocation/drops.ma       |  6 +++---
 .../lambdadelta/static_2/relocation/drops_sex.ma   |  2 +-
 .../lambdadelta/static_2/relocation/seq.ma         |  2 +-
 .../lambdadelta/static_2/relocation/sex.ma         |  6 +++---
 .../lambdadelta/static_2/relocation/sex_sex.ma     | 12 ++++++------
 .../contribs/lambdadelta/static_2/static/frees.ma  |  6 +++---
 .../lambdadelta/static_2/static/frees_drops.ma     |  4 ++--
 .../lambdadelta/static_2/static/frees_fqup.ma      |  8 ++++----
 .../contribs/lambdadelta/static_2/static/fsle.ma   |  2 +-
 .../lambdadelta/static_2/static/fsle_drops.ma      |  2 +-
 .../lambdadelta/static_2/static/fsle_fqup.ma       |  6 +++---
 .../lambdadelta/static_2/static/fsle_fsle.ma       | 14 +++++++-------
 .../contribs/lambdadelta/static_2/static/lsubf.ma  | 10 +++++-----
 .../lambdadelta/static_2/static/rex_drops.ma       |  4 ++--
 .../lambdadelta/static_2/static/rex_rex.ma         |  4 ++--
 matita/matita/predefined_virtuals.ml               |  2 +-
 56 files changed, 150 insertions(+), 150 deletions(-)
 rename matita/matita/contribs/lambdadelta/ground/notation/functions/{downspoon_2.ma => downdashedarrow_2.ma} (83%)
 rename matita/matita/contribs/lambdadelta/ground/notation/functions/{downspoonstar_3.ma => downdashedarrowstar_3.ma} (79%)
 rename matita/matita/contribs/lambdadelta/ground/notation/functions/{droppred_1.ma => downspoon_1.ma} (94%)
 rename matita/matita/contribs/lambdadelta/ground/notation/functions/{droppreds_2.ma => downspoonstar_2.ma} (92%)

diff --git a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl
index 76794da82..2c781ef57 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/apps_2/web/apps_2_src.tbl
@@ -83,7 +83,7 @@ class "capitalize italic" { 0 }
 class "italic"            { 1 }
 (*
         [ { "evaluation drop" * } {
-             [ "vdrop" + "( â«°{?}? )" + "( â«°{?}[?]? )" "vdrop_vlift" * ]
+             [ "vdrop" + "( ⇣{?}? )" + "( ⇣{?}[?]? )" "vdrop_vlift" * ]
           }
         ]
         [ { "reduction and type machine" * } {
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma
index 5ddd583d1..a23cb4ca8 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_hdtl.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/functions/downspoon_2.ma".
+include "ground/notation/functions/downdashedarrow_2.ma".
 include "ground/lib/stream.ma".
 
 (* HEAD AND TAIL FOR STREAMS ************************************************)
@@ -27,7 +27,7 @@ defined.
 
 interpretation
   "tail (streams)"
-  'DownSpoon A t = (stream_tl A t).
+  'DownDashedArrow A t = (stream_tl A t).
 
 (* Basic constructions ******************************************************)
 
@@ -36,10 +36,10 @@ lemma stream_hd_cons (A) (a) (t):
 // qed.
 
 lemma stream_tl_cons (A) (a) (t):
-      t = ⫰{A}(a⨮t).
+      t = ⇣{A}(a⨮t).
 // qed.
 
 lemma stream_split_tl (A) (t):
-      stream_hd A t ⨮ ⫰t = t.
+      stream_hd A t ⨮ ⇣t = t.
 #A * //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
index 185de605e..670790c91 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/functions/downspoonstar_3.ma".
+include "ground/notation/functions/downdashedarrowstar_3.ma".
 include "ground/lib/stream_hdtl.ma".
 include "ground/arith/nat_succ_iter.ma".
 
@@ -23,26 +23,26 @@ definition stream_tls (A) (n): stream A → stream A ≝
 
 interpretation
   "iterated tail (strams)"
-  'DownSpoonStar A n f = (stream_tls A n f).
+  'DownDashedArrowStar A n f = (stream_tls A n f).
 
 (* Basic constructions ******************************************************)
 
 lemma stream_tls_zero (A) (t):
-      t = ⫰*{A}[𝟎]t.
+      t = ⇣*{A}[𝟎]t.
 // qed.
 
 lemma stream_tls_tl (A) (n) (t):
-      (â«°â«°*[n]t) = â«°*{A}[n]â«°t.
+      (⇣⇣*[n]t) = ⇣*{A}[n]⇣t.
 #A #n #t
 @(niter_appl … (stream_tl …))
 qed.
 
 lemma stream_tls_succ (A) (n) (t):
-      (⫰⫰*[n]t) = ⫰*{A}[↑n]t.
+      (⇣⇣*[n]t) = ⇣*{A}[↑n]t.
 #A #n #t
 @(niter_succ … (stream_tl …))
 qed.
 
 lemma stream_tls_swap (A) (n) (t):
-      (⫰*[n]⫰t) = ⫰*{A}[↑n]t.
+      (⇣*[n]⇣t) = ⇣*{A}[↑n]t.
 // qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_eq.ma b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_eq.ma
index 0f65086e5..de88a638b 100644
--- a/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/lib/stream_tls_eq.ma
@@ -20,7 +20,7 @@ include "ground/lib/stream_tls.ma".
 (* Constructions with stream_eq *********************************************)
 
 lemma stream_tls_eq_repl (A) (n):
-      stream_eq_repl A (λt1,t2. ⫰*[n] t1 ≗ ⫰*[n] t2).
+      stream_eq_repl A (λt1,t2. ⇣*[n] t1 ≗ ⇣*[n] t2).
 #A #n @(nat_ind_succ … n) -n //
 #n #IH * #n1 #t1 * #n2 #t2 #H
 elim (stream_eq_inv_cons_bi … H) /2 width=7 by/
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downdashedarrow_2.ma
similarity index 83%
rename from matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_2.ma
rename to matita/matita/contribs/lambdadelta/ground/notation/functions/downdashedarrow_2.ma
index 765c2c0c3..4614cf3a3 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downdashedarrow_2.ma
@@ -14,14 +14,14 @@
 
 (* GROUND NOTATION **********************************************************)
 
-notation < "hvbox( â«° term 75 a )"
+notation < "hvbox( ⇣ term 75 a )"
   non associative with precedence 75
-  for @{ 'DownSpoon $S $a }.
+  for @{ 'DownDashedArrow $S $a }.
 
-notation > "hvbox( â«° term 75 a )"
+notation > "hvbox( ⇣ term 75 a )"
   non associative with precedence 75
-  for @{ 'DownSpoon ? $a }.
+  for @{ 'DownDashedArrow ? $a }.
 
-notation > "hvbox( â«°{ term 46 S } break term 75 a )"
+notation > "hvbox( ⇣{ term 46 S } break term 75 a )"
   non associative with precedence 75
-  for @{ 'DownSpoon $S $a }.
+  for @{ 'DownDashedArrow $S $a }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downdashedarrowstar_3.ma
similarity index 79%
rename from matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_3.ma
rename to matita/matita/contribs/lambdadelta/ground/notation/functions/downdashedarrowstar_3.ma
index 5250539d1..919695181 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_3.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downdashedarrowstar_3.ma
@@ -14,14 +14,14 @@
 
 (* GROUND NOTATION **********************************************************)
 
-notation < "hvbox( â«°*[ break term 46 n ] break term 75 a )"
+notation < "hvbox( ⇣*[ break term 46 n ] break term 75 a )"
   non associative with precedence 75
-  for @{ 'DownSpoonStar $S $n $a }.
+  for @{ 'DownDashedArrowStar $S $n $a }.
 
-notation > "hvbox( â«°*[ break term 46 n ] break term 75 a )"
+notation > "hvbox( ⇣*[ break term 46 n ] break term 75 a )"
   non associative with precedence 75
-  for @{ 'DownSpoonStar ? $n $a }.
+  for @{ 'DownDashedArrowStar ? $n $a }.
 
-notation > "hvbox( â«°*{ term 46 S }[ break term 46 n ] break term 75 a )"
+notation > "hvbox( ⇣*{ term 46 S }[ break term 46 n ] break term 75 a )"
   non associative with precedence 75
-  for @{ 'DownSpoonStar $S $n $a }.
+  for @{ 'DownDashedArrowStar $S $n $a }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/droppred_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_1.ma
similarity index 94%
rename from matita/matita/contribs/lambdadelta/ground/notation/functions/droppred_1.ma
rename to matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_1.ma
index d4e0f0354..e4bc3eb13 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/droppred_1.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoon_1.ma
@@ -14,6 +14,6 @@
 
 (* GROUND NOTATION **********************************************************)
 
-notation "hvbox( ⫱ term 75 T )"
+notation "hvbox( â«° term 75 T )"
   non associative with precedence 75
-  for @{ 'DropPred $T }.
+  for @{ 'DownSpoon $T }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/droppreds_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_2.ma
similarity index 92%
rename from matita/matita/contribs/lambdadelta/ground/notation/functions/droppreds_2.ma
rename to matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_2.ma
index 86829e053..03f188bd7 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/droppreds_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/downspoonstar_2.ma
@@ -14,6 +14,6 @@
 
 (* GROUND NOTATION **********************************************************)
 
-notation "hvbox( ⫱ *[ term 46 n ] break term 75 T )"
+notation "hvbox( â«° *[ term 46 n ] break term 75 T )"
   non associative with precedence 75
-  for @{ 'DropPreds $n $T }.
+  for @{ 'DownSpoonStar $n $T }.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_after_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_after_ist.ma
index c8051078a..ecca35eb7 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_after_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_after_ist.ma
@@ -39,7 +39,7 @@ cases (gr_after_inv_push_sn … H1f … H1) -H1f * #g21 #g #H1g #H21 #H
 | cases (gr_after_inv_push_sn_next … H2f … H1 H) -f1 -f #g22 #H2g #H22
   @(gr_eq_next … H21 H22) -f21 -f22
 ]
-@(gr_after_inj_unit_aux (⫱*[↓p]g1) … (⫱*[↓p]g)) -gr_after_inj_unit_aux
+@(gr_after_inj_unit_aux (⫰*[↓p]g1) … (⫰*[↓p]g)) -gr_after_inj_unit_aux
 /2 width=1 by gr_after_tls_sn_tls, gr_ist_tls, gr_pat_unit_succ_tls/
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni_tls.ma
index cef9bd7e4..632d35f6c 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_nat_uni_tls.ma
@@ -24,7 +24,7 @@ include "ground/relocation/gr_after_isi.ma".
 (*** after_uni_dx *)
 lemma gr_after_nat_uni (l2) (l1):
       ∀f2. @↑❪l1, f2❫ ≘ l2 →
-      ∀f. f2 ⊚ 𝐮❨l1❩ ≘ f → 𝐮❨l2❩ ⊚ ⫱*[l2] f2 ≘ f.
+      ∀f. f2 ⊚ 𝐮❨l1❩ ≘ f → 𝐮❨l2❩ ⊚ ⫰*[l2] f2 ≘ f.
 #l2 @(nat_ind_succ … l2) -l2
 [ #l1 #f2 #Hf2 #f #Hf
   elim (gr_nat_inv_zero_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
@@ -45,7 +45,7 @@ qed.
 (*** after_uni_sn *)
 lemma gr_nat_after_uni_tls (l2) (l1):
       ∀f2. @↑❪l1, f2❫ ≘ l2 →
-      ∀f. 𝐮❨l2❩ ⊚ ⫱*[l2] f2 ≘ f → f2 ⊚ 𝐮❨l1❩ ≘ f.
+      ∀f. 𝐮❨l2❩ ⊚ ⫰*[l2] f2 ≘ f → f2 ⊚ 𝐮❨l1❩ ≘ f.
 #l2 @(nat_ind_succ … l2) -l2
 [ #l1 #f2 #Hf2 #f #Hf
   elim (gr_nat_inv_zero_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_tls.ma
index b7b5fc7fb..4c0623e6e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_tls.ma
@@ -24,7 +24,7 @@ include "ground/relocation/gr_after.ma".
 (*** after_tls *)
 lemma gr_after_tls_sn_tls (n):
       ∀f1,f2,f. @❪𝟏, f1❫ ≘ ↑n →
-      f1 ⊚ f2 ≘ f → ⫱*[n]f1 ⊚ f2 ≘ ⫱*[n]f.
+      f1 ⊚ f2 ≘ f → ⫰*[n]f1 ⊚ f2 ≘ ⫰*[n]f.
 #n @(nat_ind_succ … n) -n //
 #n #IH #f1 #f2 #f #Hf1 #Hf
 cases (gr_pat_inv_unit_succ … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni_tls.ma
index 40853b262..fe1286668 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_after_pat_uni_tls.ma
@@ -25,7 +25,7 @@ include "ground/relocation/gr_after_isi.ma".
 (*** after_uni_succ_dx *)
 lemma gr_after_pat_uni (i2) (i1):
       ∀f2. @❪i1, f2❫ ≘ i2 →
-      ∀f. f2 ⊚ 𝐮❨i1❩ ≘ f → 𝐮❨i2❩ ⊚ ⫱*[i2] f2 ≘ f.
+      ∀f. f2 ⊚ 𝐮❨i1❩ ≘ f → 𝐮❨i2❩ ⊚ ⫰*[i2] f2 ≘ f.
 #i2 elim i2 -i2
 [ #i1 #f2 #Hf2 #f #Hf
   elim (gr_pat_inv_unit_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
@@ -47,7 +47,7 @@ qed.
 (*** after_uni_succ_sn *)
 lemma gr_pat_after_uni_tls (i2) (i1):
       ∀f2. @❪i1, f2❫ ≘ i2 →
-      ∀f. 𝐮❨i2❩ ⊚ ⫱*[i2] f2 ≘ f → f2 ⊚ 𝐮❨i1❩ ≘ f.
+      ∀f. 𝐮❨i2❩ ⊚ ⫰*[i2] f2 ≘ f → f2 ⊚ 𝐮❨i1❩ ≘ f.
 #i2 elim i2 -i2
 [ #i1 #f2 #Hf2 #f #Hf
   elim (gr_pat_inv_unit_dx … Hf2) -Hf2 // #g2 #H1 #H2 destruct
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter.ma
index bbac0036c..2ec6991cf 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter.ma
@@ -217,8 +217,8 @@ qed-.
 
 (*** coafter_inv_tl1 *)
 lemma gr_coafter_inv_tl_dx:
-      ∀g2,g1,g. g2 ~⊚ ⫱g1 ≘ g →
-      ∃∃f. ⫯g2 ~⊚ g1 ≘ f & ⫱f = g.
+      ∀g2,g1,g. g2 ~⊚ ⫰g1 ≘ g →
+      ∃∃f. ⫯g2 ~⊚ g1 ≘ f & ⫰f = g.
 #g2 #g1 #g
 elim (gr_map_split_tl g1) #H1 #H2
 [ /3 width=7 by gr_coafter_refl, ex2_intro/
@@ -228,8 +228,8 @@ qed-.
 
 (*** coafter_inv_tl0 *)
 lemma gr_coafter_inv_tl:
-      ∀g2,g1,g. g2 ~⊚ g1 ≘ ⫱g →
-      ∃∃f1. ⫯g2 ~⊚ f1 ≘ g & ⫱f1 = g1.
+      ∀g2,g1,g. g2 ~⊚ g1 ≘ ⫰g →
+      ∃∃f1. ⫯g2 ~⊚ f1 ≘ g & ⫰f1 = g1.
 #g2 #g1 #g
 elim (gr_map_split_tl g) #H1 #H2
 [ /3 width=7 by gr_coafter_refl, ex2_intro/
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_coafter_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_coafter_ist.ma
index f1e633463..9d79801dc 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_coafter_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_coafter_ist.ma
@@ -38,7 +38,7 @@ cases (gr_coafter_inv_push_sn … H1f … H1) -H1f * #g21 #g #H1g #H21 #H
 | cases (gr_coafter_inv_push_sn_next … H2f … H1 H) -f1 -f #g22 #H2g #H22
   @(gr_eq_next … H21 H22) -f21 -f22
 ]
-@(gr_coafter_inj_unit_aux (⫱*[↓n]g1) … (⫱*[↓n]g)) -gr_coafter_inj_unit_aux
+@(gr_coafter_inj_unit_aux (⫰*[↓n]g1) … (⫰*[↓n]g)) -gr_coafter_inj_unit_aux
 /2 width=1 by gr_coafter_tls_bi_tls, gr_ist_tls, gr_pat_unit_succ_tls/
 qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_nat_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_nat_tls.ma
index 6d953f203..0402e2929 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_nat_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_nat_tls.ma
@@ -23,7 +23,7 @@ include "ground/relocation/gr_coafter.ma".
 (*** coafter_tls *)
 lemma gr_coafter_tls_bi_tls (n2) (n1):
       ∀f1,f2,f. @↑❪n1, f1❫ ≘ n2 →
-      f1 ~⊚ f2 ≘ f → ⫱*[n2]f1 ~⊚ ⫱*[n1]f2 ≘ ⫱*[n2]f.
+      f1 ~⊚ f2 ≘ f → ⫰*[n2]f1 ~⊚ ⫰*[n1]f2 ≘ ⫰*[n2]f.
 #n2 @(nat_ind_succ … n2) -n2 [ #n1 | #n2 #IH * [| #n1 ] ] #f1 #f2 #f #Hf1 #Hf
 [ elim (gr_nat_inv_zero_dx … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1 destruct //
 | elim (gr_nat_inv_zero_succ … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1
@@ -41,5 +41,5 @@ qed.
 (*** coafter_tls_O *)
 lemma gr_coafter_tls_sn_tls:
       ∀n,f1,f2,f. @↑❪𝟎, f1❫ ≘ n →
-      f1 ~⊚ f2 ≘ f → ⫱*[n]f1 ~⊚ f2 ≘ ⫱*[n]f.
+      f1 ~⊚ f2 ≘ f → ⫰*[n]f1 ~⊚ f2 ≘ ⫰*[n]f.
 /2 width=1 by gr_coafter_tls_bi_tls/ qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_nat_tls_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_nat_tls_pushs.ma
index 524e1d881..d42709290 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_nat_tls_pushs.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_nat_tls_pushs.ma
@@ -24,7 +24,7 @@ include "ground/relocation/gr_coafter.ma".
 (*** coafter_fwd_pushs *)
 lemma gr_coafter_des_pushs_dx (n) (m):
       ∀g2,f1,g. g2 ~⊚ ⫯*[m]f1 ≘ g → @↑❪m, g2❫ ≘ n →
-      ∃∃f. ⫱*[n]g2 ~⊚ f1 ≘ f & ⫯*[n] f = g.
+      ∃∃f. ⫰*[n]g2 ~⊚ f1 ≘ f & ⫯*[n] f = g.
 #n @(nat_ind_succ … n) -n
 [ #m #g2 #f1 #g #Hg #H
   elim (gr_nat_inv_zero_dx … H) -H [|*: // ] #f2 #H1 #H2 destruct
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_pat_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_pat_tls.ma
index a2c00145b..529b4caa5 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_pat_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_coafter_pat_tls.ma
@@ -23,7 +23,7 @@ include "ground/relocation/gr_coafter_nat_tls.ma".
 (*** coafter_tls_succ *)
 lemma gr_coafter_tls_tl_tls:
       ∀g2,g1,g. g2 ~⊚ g1 ≘ g →
-      ∀j. @❪𝟏, g2❫ ≘ j → ⫱*[j]g2 ~⊚ ⫱g1 ≘ ⫱*[j]g.
+      ∀j. @❪𝟏, g2❫ ≘ j → ⫰*[j]g2 ~⊚ ⫰g1 ≘ ⫰*[j]g.
 #g2 #g1 #g #Hg #j #Hg2
 lapply (gr_nat_pred_bi … Hg2) -Hg2 #Hg2
 lapply (gr_coafter_tls_bi_tls … Hg2 … Hg) -Hg #Hg
@@ -36,7 +36,7 @@ qed.
 (* Note: parked for now
 lemma coafter_fwd_xpx_pushs:
       ∀g2,f1,g,i,j. @❪i, g2❫ ≘ j → g2 ~⊚ ⫯*[i]⫯f1 ≘ g →
-      ∃∃f.  ⫱*[↑j]g2 ~⊚ f1 ≘ f & ⫯*[j]⫯f = g.
+      ∃∃f.  ⫰*[↑j]g2 ~⊚ f1 ≘ f & ⫯*[j]⫯f = g.
 #g2 #g1 #g #i #j #Hg2 <pushs_xn #Hg(coafter_fwd_pushs … Hg Hg2) #f #H0 destruct
 lapply (coafter_tls … Hg2 Hg) -Hg <tls_pushs <tls_pushs #Hf
 lapply (at_inv_tls … Hg2) -Hg2 #H
@@ -47,7 +47,7 @@ qed-.
 
 lemma coafter_fwd_xnx_pushs:
       ∀g2,f1,g,i,j. @❪i, g2❫ ≘ j → g2 ~⊚ ⫯*[i]↑f1 ≘ g →
-      ∃∃f. ⫱*[↑j]g2 ~⊚ f1 ≘ f & ⫯*[j] ↑f = g.
+      ∃∃f. ⫰*[↑j]g2 ~⊚ f1 ≘ f & ⫯*[j] ↑f = g.
 #g2 #g1 #g #i #j #Hg2 #Hg
 elim (coafter_fwd_pushs … Hg Hg2) #f #H0 destruct
 lapply (coafter_tls … Hg2 Hg) -Hg <tls_pushs <tls_pushs #Hf
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_tl.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_tl.ma
index 05a3505e1..43e865131 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_tl.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_tl.ma
@@ -20,7 +20,7 @@ include "ground/relocation/gr_isd.ma".
 (* Constructions with gr_tl *************************************************)
 
 (*** isdiv_tl *)
-lemma gr_isd_tl (f): 𝛀❪f❫ → 𝛀❪⫱f❫.
+lemma gr_isd_tl (f): 𝛀❪f❫ → 𝛀❪⫰f❫.
 #f cases (gr_map_split_tl f) * #H
 [ elim (gr_isd_inv_push … H) -H //
 | /2 width=3 by gr_isd_inv_next/
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_tls.ma
index 3bea6fb18..dc5b123cc 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isd_tls.ma
@@ -20,6 +20,6 @@ include "ground/relocation/gr_isd_tl.ma".
 (* Constructions with gr_tls ************************************************)
 
 (*** isdiv_tls *)
-lemma gr_isd_tls (n) (g): 𝛀❪g❫ → 𝛀❪⫱*[n]g❫.
+lemma gr_isd_tls (n) (g): 𝛀❪g❫ → 𝛀❪⫰*[n]g❫.
 #n @(nat_ind_succ … n) -n /3 width=1 by gr_isd_tl/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_tl.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_tl.ma
index 52bc146fe..5268136d7 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_tl.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_tl.ma
@@ -20,7 +20,7 @@ include "ground/relocation/gr_isf.ma".
 (* Constructions with gr_tl *************************************************)
 
 (*** isfin_tl *)
-lemma gr_isf_tl (f): 𝐅❪f❫ → 𝐅❪⫱f❫.
+lemma gr_isf_tl (f): 𝐅❪f❫ → 𝐅❪⫰f❫.
 #f elim (gr_map_split_tl f) * #Hf
 /3 width=3 by gr_isf_inv_push, gr_isf_inv_next/
 qed.
@@ -28,7 +28,7 @@ qed.
 (* Inversions with gr_tl ****************************************************)
 
 (*** isfin_inv_tl *)
-lemma gr_isf_inv_tl (g): 𝐅❪⫱g❫ → 𝐅❪g❫.
+lemma gr_isf_inv_tl (g): 𝐅❪⫰g❫ → 𝐅❪g❫.
 #f elim (gr_map_split_tl f) * #Hf
 /2 width=1 by gr_isf_next, gr_isf_push/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_tls.ma
index ebd7a36e2..3815a74a3 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isf_tls.ma
@@ -19,13 +19,13 @@ include "ground/relocation/gr_isf_tl.ma".
 
 (* Constructions with gr_tls ************************************************)
 
-lemma gr_isf_tls (n) (f): 𝐅❪f❫ → 𝐅❪⫱*[n]f❫.
+lemma gr_isf_tls (n) (f): 𝐅❪f❫ → 𝐅❪⫰*[n]f❫.
 #n @(nat_ind_succ … n) -n /3 width=1 by gr_isf_tl/
 qed.
 
 (* Inversions with gr_tls ***************************************************)
 
 (*** isfin_inv_tls *)
-lemma gr_isf_inv_tls (n) (g): 𝐅❪⫱*[n]g❫ → 𝐅❪g❫.
+lemma gr_isf_inv_tls (n) (g): 𝐅❪⫰*[n]g❫ → 𝐅❪g❫.
 #n @(nat_ind_succ … n) -n /3 width=1 by gr_isf_inv_tl/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tl.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tl.ma
index abf089d54..0246557f3 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tl.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tl.ma
@@ -20,7 +20,7 @@ include "ground/relocation/gr_isi.ma".
 (* Constructions with gr_tl *************************************************)
 
 (*** isid_tl *)
-lemma gr_isi_tl (f): 𝐈❪f❫ → 𝐈❪⫱f❫.
+lemma gr_isi_tl (f): 𝐈❪f❫ → 𝐈❪⫰f❫.
 #f cases (gr_map_split_tl f) * #H
 [ /2 width=3 by gr_isi_inv_push/
 | elim (gr_isi_inv_next … H) -H //
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tls.ma
index cdef65ddb..05881cbb5 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isi_tls.ma
@@ -20,6 +20,6 @@ include "ground/relocation/gr_isi_tl.ma".
 (* Constructions with gr_tls ************************************************)
 
 (*** isid_tls *)
-lemma gr_isi_tls (n) (f): 𝐈❪f❫ → 𝐈❪⫱*[n]f❫.
+lemma gr_isi_tls (n) (f): 𝐈❪f❫ → 𝐈❪⫰*[n]f❫.
 #n @(nat_ind_succ … n) -n /3 width=1 by gr_isi_tl/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist.ma
index 8a3636574..d7f511a56 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist.ma
@@ -42,7 +42,7 @@ qed-.
 (* Constructions with gr_tl *************************************************)
 
 (*** istot_tl *)
-lemma gr_ist_tl (f): 𝐓❪f❫ → 𝐓❪⫱f❫.
+lemma gr_ist_tl (f): 𝐓❪f❫ → 𝐓❪⫰f❫.
 #f cases (gr_map_split_tl f) *
 /2 width=3 by gr_ist_inv_next, gr_ist_inv_push/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_tls.ma
index e1c04930a..e6da8edd3 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_ist_tls.ma
@@ -20,7 +20,7 @@ include "ground/relocation/gr_ist.ma".
 (* Constructions with gr_tls ************************************************)
 
 (*** istot_tls *)
-lemma gr_ist_tls (n) (f): 𝐓❪f❫ → 𝐓❪⫱*[n]f❫.
+lemma gr_ist_tls (n) (f): 𝐓❪f❫ → 𝐓❪⫰*[n]f❫.
 #n @(nat_ind_succ … n) -n //
 #n #IH #f #Hf <gr_tls_succ
 /3 width=1 by gr_ist_tl/
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu_tl.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu_tl.ma
index 73fa585b7..8a7b07df1 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu_tl.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_isu_tl.ma
@@ -19,7 +19,7 @@ include "ground/relocation/gr_isu.ma".
 
 (* Constructions with gr_tl *************************************************)
 
-lemma gr_isu_tl (f): 𝐔❪f❫ → 𝐔❪⫱f❫.
+lemma gr_isu_tl (f): 𝐔❪f❫ → 𝐔❪⫰f❫.
 #f cases (gr_map_split_tl f) * #H
 [ /3 width=3 by gr_isu_inv_push, gr_isu_isi/
 | /2 width=3 by gr_isu_inv_next/
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_lt.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_lt.ma
index 8fc080ed6..648c27f71 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_lt.ma
@@ -40,7 +40,7 @@ lemma gr_pat_increasing_strict (g) (i1) (i2):
 qed-.
 
 (*** at_fwd_id_ex *)
-lemma gr_pat_des_id (f) (i): @❪i,f❫ ≘ i → ⫯⫱f = f.
+lemma gr_pat_des_id (f) (i): @❪i,f❫ ≘ i → ⫯⫰f = f.
 #f elim (gr_map_split_tl f) //
 #H #i #Hf elim (gr_pat_inv_next … Hf … H) -Hf -H
 #j2 #Hg #H destruct lapply (gr_pat_increasing … Hg) -Hg
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_tls.ma
index 1eca80ecf..f31d01b5d 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_pat_tls.ma
@@ -23,7 +23,7 @@ include "ground/relocation/gr_pat_eq.ma".
 (* Note: this requires ↑ on first n *)
 (*** at_pxx_tls *)
 lemma gr_pat_unit_succ_tls (n) (f):
-      @❪𝟏,f❫ ≘ ↑n → @❪𝟏,⫱*[n]f❫ ≘ 𝟏.
+      @❪𝟏,f❫ ≘ ↑n → @❪𝟏,⫰*[n]f❫ ≘ 𝟏.
 #n @(nat_ind_succ … n) -n //
 #n #IH #f #Hf
 elim (gr_pat_inv_unit_succ … Hf) -Hf [|*: // ] #g #Hg #H0 destruct
@@ -32,7 +32,7 @@ qed.
 
 (* Note: this requires ↑ on third n2 *)
 (*** at_tls *)
-lemma gr_pat_tls (n2) (f): ⫯⫱*[↑n2]f ≡ ⫱*[n2]f → ∃i1. @❪i1,f❫ ≘ ↑n2.
+lemma gr_pat_tls (n2) (f): ⫯⫰*[↑n2]f ≡ ⫰*[n2]f → ∃i1. @❪i1,f❫ ≘ ↑n2.
 #n2 @(nat_ind_succ … n2) -n2
 [ /4 width=4 by gr_pat_eq_repl_back, gr_pat_refl, ex_intro/
 | #n2 #IH #f <gr_tls_swap <gr_tls_swap in ⊢ (??%→?); #H
@@ -48,7 +48,7 @@ qed-.
 (*** at_inv_nxx *)
 lemma gr_pat_inv_succ_sn (p) (g) (i1) (j2):
       @❪↑i1,g❫ ≘ j2 → @❪𝟏,g❫ ≘ p →
-      ∃∃i2. @❪i1,⫱*[p]g❫ ≘ i2 & p+i2 = j2.
+      ∃∃i2. @❪i1,⫰*[p]g❫ ≘ i2 & p+i2 = j2.
 #p elim p -p
 [ #g #i1 #j2 #Hg #H
   elim (gr_pat_inv_unit_bi … H) -H [|*: // ] #f #H0
@@ -65,7 +65,7 @@ qed-.
 (* Note: this requires ↑ on first n2 *)
 (*** at_inv_tls *)
 lemma gr_pat_inv_succ_dx_tls (n2) (i1) (f):
-      @❪i1,f❫ ≘ ↑n2 → ⫯⫱*[↑n2]f ≡ ⫱*[n2]f.
+      @❪i1,f❫ ≘ ↑n2 → ⫯⫰*[↑n2]f ≡ ⫰*[n2]f.
 #n2 @(nat_ind_succ … n2) -n2
 [ #i1 #f #Hf elim (gr_pat_inv_unit_dx … Hf) -Hf // #g #H1 #H destruct
   /2 width=1 by gr_eq_refl/
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle.ma
index 8aec4d513..74c15789f 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle.ma
@@ -124,21 +124,21 @@ qed-.
 
 (*** sle_px_tl *)
 lemma gr_sle_push_sn_tl:
-      ∀g1,g2. g1 ⊆ g2 → ∀f1. ⫯f1 = g1 → f1 ⊆ ⫱g2.
+      ∀g1,g2. g1 ⊆ g2 → ∀f1. ⫯f1 = g1 → f1 ⊆ ⫰g2.
 #g1 #g2 #H #f1 #H1
 elim (gr_sle_inv_push_sn … H … H1) -H -H1 * //
 qed.
 
 (*** sle_xn_tl *)
 lemma gr_sle_next_dx_tl:
-      ∀g1,g2. g1 ⊆ g2 → ∀f2. ↑f2 = g2 → ⫱g1 ⊆ f2.
+      ∀g1,g2. g1 ⊆ g2 → ∀f2. ↑f2 = g2 → ⫰g1 ⊆ f2.
 #g1 #g2 #H #f2 #H2
 elim (gr_sle_inv_next_dx … H … H2) -H -H2 * //
 qed.
 
 (*** sle_tl *)
 lemma gr_sle_tl:
-      ∀f1,f2. f1 ⊆ f2 → ⫱f1 ⊆ ⫱f2.
+      ∀f1,f2. f1 ⊆ f2 → ⫰f1 ⊆ ⫰f2.
 #f1 elim (gr_map_split_tl f1) #H1 #f2 #H
 [ lapply (gr_sle_push_sn_tl … H … H1) -H //
 | elim (gr_sle_inv_next_sn … H … H1) -H //
@@ -149,14 +149,14 @@ qed.
 
 (*** sle_inv_tl_sn *)
 lemma gr_sle_inv_tl_sn:
-      ∀f1,f2. ⫱f1 ⊆ f2 → f1 ⊆ ↑f2.
+      ∀f1,f2. ⫰f1 ⊆ f2 → f1 ⊆ ↑f2.
 #f1 elim (gr_map_split_tl f1) #H #f2 #Hf12
 /2 width=5 by gr_sle_next, gr_sle_weak/
 qed-.
 
 (*** sle_inv_tl_dx *)
 lemma gr_sle_inv_tl_dx:
-      ∀f1,f2. f1 ⊆ ⫱f2 → ⫯f1 ⊆ f2.
+      ∀f1,f2. f1 ⊆ ⫰f2 → ⫯f1 ⊆ f2.
 #f1 #f2 elim (gr_map_split_tl f2) #H #Hf12
 /2 width=5 by gr_sle_push, gr_sle_weak/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_tls.ma
index ac4300633..ea319ccda 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sle_tls.ma
@@ -21,7 +21,7 @@ include "ground/relocation/gr_sle.ma".
 
 (*** sle_tls *)
 lemma gr_sle_tls:
-      ∀f1,f2. f1 ⊆ f2 → ∀n. ⫱*[n] f1 ⊆ ⫱*[n] f2.
+      ∀f1,f2. f1 ⊆ f2 → ∀n. ⫰*[n] f1 ⊆ ⫰*[n] f2.
 #f1 #f2 #Hf12 #n @(nat_ind_succ … n) -n
 /2 width=5 by gr_sle_tl/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor.ma
index 54911325e..4f2e759e0 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor.ma
@@ -281,7 +281,7 @@ qed-.
 
 (*** sor_tl *)
 lemma gr_sor_tl:
-      ∀f1,f2,f. f1 ⋓ f2 ≘ f → ⫱f1 ⋓ ⫱f2 ≘ ⫱f.
+      ∀f1,f2,f. f1 ⋓ f2 ≘ f → ⫰f1 ⋓ ⫰f2 ≘ ⫰f.
 #f1 cases (gr_map_split_tl f1) #H1
 #f2 cases (gr_map_split_tl f2) #H2
 #f #Hf
@@ -295,8 +295,8 @@ qed.
 (*** sor_xxn_tl *)
 lemma gr_sor_next_tl:
       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f. ↑f = g →
-      (∃∃f1,f2. f1 ⋓ f2 ≘ f & ↑f1 = g1 & ⫱g2 = f2) ∨
-      (∃∃f1,f2. f1 ⋓ f2 ≘ f & ⫱g1 = f1 & ↑f2 = g2).
+      (∃∃f1,f2. f1 ⋓ f2 ≘ f & ↑f1 = g1 & ⫰g2 = f2) ∨
+      (∃∃f1,f2. f1 ⋓ f2 ≘ f & ⫰g1 = f1 & ↑f2 = g2).
 #g1 #g2 #g #H #f #H0 elim (gr_sor_inv_next … H … H0) -H -H0 *
 /3 width=5 by ex3_2_intro, or_introl, or_intror/
 qed-.
@@ -304,7 +304,7 @@ qed-.
 (*** sor_xnx_tl *)
 lemma gr_sor_next_dx_tl:
       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f2. ↑f2 = g2 →
-      ∃∃f1,f. f1 ⋓ f2 ≘ f & ⫱g1 = f1 & ↑f = g.
+      ∃∃f1,f. f1 ⋓ f2 ≘ f & ⫰g1 = f1 & ↑f = g.
 #g1 elim (gr_map_split_tl g1) #H1 #g2 #g #H #f2 #H2
 [ elim (gr_sor_inv_push_next … H … H1 H2)
 | elim (gr_sor_inv_next_bi … H … H1 H2)
@@ -315,7 +315,7 @@ qed-.
 (*** sor_nxx_tl *)
 lemma gr_sor_next_sn_tl:
       ∀g1,g2,g. g1 ⋓ g2 ≘ g → ∀f1. ↑f1 = g1 →
-      ∃∃f2,f. f1 ⋓ f2 ≘ f & ⫱g2 = f2 & ↑f = g.
+      ∃∃f2,f. f1 ⋓ f2 ≘ f & ⫰g2 = f2 & ↑f = g.
 #g1 #g2 elim (gr_map_split_tl g2) #H2 #g #H #f1 #H1
 [ elim (gr_sor_inv_next_push … H … H1 H2)
 | elim (gr_sor_inv_next_bi … H … H1 H2)
@@ -327,14 +327,14 @@ qed-.
 
 (*** sor_inv_tl_sn *)
 lemma gr_sor_inv_tl_sn:
-      ∀f1,f2,f. ⫱f1 ⋓ f2 ≘ f → f1 ⋓ ↑f2 ≘ ↑f.
+      ∀f1,f2,f. ⫰f1 ⋓ f2 ≘ f → f1 ⋓ ↑f2 ≘ ↑f.
 #f1 #f2 #f elim (gr_map_split_tl f1)
 /2 width=7 by gr_sor_push_next, gr_sor_next_bi/
 qed-.
 
 (*** sor_inv_tl_dx *)
 lemma gr_sor_inv_tl_dx:
-      ∀f1,f2,f. f1 ⋓ ⫱f2 ≘ f → ↑f1 ⋓ f2 ≘ ↑f.
+      ∀f1,f2,f. f1 ⋓ ⫰f2 ≘ f → ↑f1 ⋓ f2 ≘ ↑f.
 #f1 #f2 #f elim (gr_map_split_tl f2)
 /2 width=7 by gr_sor_next_push, gr_sor_next_bi/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_tls.ma
index 82e447995..33a55aa15 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_sor_tls.ma
@@ -22,7 +22,7 @@ include "ground/relocation/gr_sor.ma".
 (*** sor_tls *)
 lemma gr_sor_tls:
       ∀f1,f2,f. f1 ⋓ f2 ≘ f →
-      ∀n. ⫱*[n]f1 ⋓ ⫱*[n]f2 ≘ ⫱*[n]f.
+      ∀n. ⫰*[n]f1 ⋓ ⫰*[n]f2 ≘ ⫰*[n]f.
 #f1 #f2 #f #Hf #n @(nat_ind_succ … n) -n
 /2 width=1 by gr_sor_tl/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl.ma
index c0d15ce19..909430cd9 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl.ma
@@ -12,32 +12,32 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/functions/droppred_1.ma".
+include "ground/notation/functions/downspoon_1.ma".
 include "ground/lib/stream_hdtl.ma".
 include "ground/relocation/gr_map.ma".
 
 (* TAIL FOR GENERIC RELOCATION MAPS *****************************************)
 
 (*** tl *)
-definition gr_tl (f): gr_map ≝ ⫰f.
+definition gr_tl (f): gr_map ≝ ⇣f.
 
 interpretation
   "tail (generic relocation maps)"
-  'DropPred f = (gr_tl f).
+  'DownSpoon f = (gr_tl f).
 
 (* Basic constructions ******************************************************)
 
 (*** tl_push_rew *)
-lemma gr_tl_push (f): f = ⫱⫯f.
+lemma gr_tl_push (f): f = ⫰⫯f.
 // qed.
 
 (*** tl_next_rew *)
-lemma gr_tl_next (f): f = ⫱↑f.
+lemma gr_tl_next (f): f = ⫰↑f.
 // qed.
 
 (* Basic eliminations *******************************************************)
 
 (*** pn_split gr_map_split *)
-lemma gr_map_split_tl (f): ∨∨ ⫯⫱f = f | ↑⫱f = f.
+lemma gr_map_split_tl (f): ∨∨ ⫯⫰f = f | ↑⫰f = f.
 * * /2 width=1 by or_introl, or_intror/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl_eq.ma
index d93e7215f..e5f9897c7 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tl_eq.ma
@@ -27,7 +27,7 @@ qed.
 
 (*** tl_eq_repl *)
 lemma gr_tl_eq_repl:
-      gr_eq_repl … (λf1,f2. ⫱f1 ≡ ⫱f2).
+      gr_eq_repl … (λf1,f2. ⫰f1 ≡ ⫰f2).
 #f1 #f2 * -f1 -f2 //
 qed.
 
@@ -36,8 +36,8 @@ qed.
 (*** eq_inv_gen *)
 lemma gr_eq_inv_gen (g1) (g2):
       g1 ≡ g2 →
-      ∨∨ ∧∧ ⫱g1 ≡ ⫱g2 & ⫯⫱g1 = g1 & ⫯⫱g2 = g2
-       | ∧∧ ⫱g1 ≡ ⫱g2 & ↑⫱g1 = g1 & ↑⫱g2 = g2.
+      ∨∨ ∧∧ ⫰g1 ≡ ⫰g2 & ⫯⫰g1 = g1 & ⫯⫰g2 = g2
+       | ∧∧ ⫰g1 ≡ ⫰g2 & ↑⫰g1 = g1 & ↑⫰g2 = g2.
 #g1 #g2 * -g1 -g2 #f1 #f2 #g1 #g2 #f * *
 /3 width=1 by and3_intro, or_introl, or_intror/
 qed-.
@@ -47,7 +47,7 @@ qed-.
 (*** gr_eq_inv_px *)
 lemma gr_eq_inv_push_sn (g1) (g2):
       g1 ≡ g2 → ∀f1. ⫯f1 = g1 →
-      ∧∧ f1 ≡ ⫱g2 & ⫯⫱g2 = g2.
+      ∧∧ f1 ≡ ⫰g2 & ⫯⫰g2 = g2.
 #g1 #g2 #H #f1 #Hf1
 elim (gr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
 [ /2 width=1 by conj/
@@ -58,7 +58,7 @@ qed-.
 (*** gr_eq_inv_nx *)
 lemma gr_eq_inv_next_sn (g1) (g2):
       g1 ≡ g2 → ∀f1. ↑f1 = g1 →
-      ∧∧ f1 ≡ ⫱g2 & ↑⫱g2 = g2.
+      ∧∧ f1 ≡ ⫰g2 & ↑⫰g2 = g2.
 #g1 #g2 #H #f1 #Hf1
 elim (gr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
 [ elim (eq_inv_gr_push_next … Hg1)
@@ -69,7 +69,7 @@ qed-.
 (*** gr_eq_inv_xp *)
 lemma gr_eq_inv_push_dx (g1) (g2):
       g1 ≡ g2 → ∀f2. ⫯f2 = g2 →
-      ∧∧ ⫱g1 ≡ f2 & ⫯⫱g1 = g1.
+      ∧∧ ⫰g1 ≡ f2 & ⫯⫰g1 = g1.
 #g1 #g2 #H #f2 #Hf2
 elim (gr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
 [ /2 width=1 by conj/
@@ -80,7 +80,7 @@ qed-.
 (*** gr_eq_inv_xn *)
 lemma gr_eq_inv_next_dx (g1) (g2):
       g1 ≡ g2 → ∀f2. ↑f2 = g2 →
-      ∧∧ ⫱g1 ≡ f2 & ↑⫱g1 = g1.
+      ∧∧ ⫰g1 ≡ f2 & ↑⫰g1 = g1.
 #g1 #g2 #H #f2 #Hf2
 elim (gr_eq_inv_gen … H) -H * #Hg #Hg1 #Hg2 destruct
 [ elim (eq_inv_gr_push_next … Hg2)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma
index e6134e7f9..d15047b0c 100644
--- 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) ≝ ⫰*[n]f.
+definition gr_tls (n) (f:gr_map) ≝ ⇣*[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.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_eq.ma
index 4c6dcda00..0cc631686 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_eq.ma
@@ -21,6 +21,6 @@ include "ground/relocation/gr_tls.ma".
 
 (*** tls_eq_repl *)
 lemma gr_tls_eq_repl (n):
-      gr_eq_repl (λf1,f2. ⫱*[n] f1 ≡ ⫱*[n] f2).
+      gr_eq_repl (λf1,f2. ⫰*[n] f1 ≡ ⫰*[n] f2).
 #n @(nat_ind_succ … n) -n /3 width=1 by gr_tl_eq_repl/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_nexts_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_nexts_eq.ma
index 7934c2e3a..a0d4e3910 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_nexts_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_nexts_eq.ma
@@ -22,7 +22,7 @@ include "ground/relocation/gr_tls_eq.ma".
 (*** eq_inv_nexts_sn *)
 lemma gr_eq_inv_nexts_sn (n):
       ∀f1,g2. ↑*[n] f1 ≡ g2 →
-      ∧∧ f1 ≡ ⫱*[n]g2 & ↑*[n]⫱*[n]g2 = g2.
+      ∧∧ f1 ≡ ⫰*[n]g2 & ↑*[n]⫰*[n]g2 = g2.
 #n @(nat_ind_succ … n) -n /2 width=1 by conj/
 #n #IH #f1 #g2 #H
 elim (gr_eq_inv_next_sn … H) -H [|*: // ] #Hf10 *
@@ -33,7 +33,7 @@ qed-.
 (*** eq_inv_nexts_dx *)
 lemma gr_eq_inv_nexts_dx (n):
       ∀f2,g1. g1 ≡ ↑*[n] f2 →
-      ∧∧ ⫱*[n]g1 ≡ f2 & ↑*[n]⫱*[n]g1 = g1.
+      ∧∧ ⫰*[n]g1 ≡ f2 & ↑*[n]⫰*[n]g1 = g1.
 #n @(nat_ind_succ … n) -n /2 width=1 by conj/
 #n #IH #f2 #g1 #H
 elim (gr_eq_inv_next_dx … H) -H [|*: // ] #Hf02 *
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs.ma
index bcce1e8c8..1bc1578d7 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs.ma
@@ -20,7 +20,7 @@ include "ground/relocation/gr_tls.ma".
 (* Constructions with gr_pushs **********************************************)
 
 (*** tls_pushs *)
-lemma gr_tls_pushs (n) (f): f = ⫱*[n] ⫯*[n] f.
+lemma gr_tls_pushs (n) (f): f = ⫰*[n] ⫯*[n] f.
 #n @(nat_ind_succ … n) -n //
 #n #IH #f <gr_tls_swap <gr_pushs_succ <gr_tl_push //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs_eq.ma
index db5e705a3..2193d8dd9 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls_pushs_eq.ma
@@ -22,7 +22,7 @@ include "ground/relocation/gr_pushs.ma".
 (*** eq_inv_pushs_sn *)
 lemma gr_eq_inv_pushs_sn (n):
       ∀f1,g2. ⫯*[n] f1 ≡ g2 →
-      ∧∧ f1 ≡ ⫱*[n]g2 & ⫯*[n]⫱*[n]g2 = g2.
+      ∧∧ f1 ≡ ⫰*[n]g2 & ⫯*[n]⫰*[n]g2 = g2.
 #n @(nat_ind_succ … n) -n /2 width=1 by conj/
 #n #IH #f1 #g2 #H
 elim (gr_eq_inv_push_sn … H) -H [|*: // ] #Hf10 *
@@ -33,7 +33,7 @@ qed-.
 (*** eq_inv_pushs_dx *)
 lemma gr_eq_inv_pushs_dx (n):
       ∀f2,g1. g1 ≡ ⫯*[n] f2 →
-      ∧∧ ⫱*[n]g1 ≡ f2 & ⫯*[n]⫱*[n]g1 = g1.
+      ∧∧ ⫰*[n]g1 ≡ f2 & ⫯*[n]⫰*[n]g1 = g1.
 #n @(nat_ind_succ … n) -n /2 width=1 by conj/
 #n #IH #f2 #g1 #H
 elim (gr_eq_inv_push_dx … H) -H [|*: // ] #Hf02 *
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 3646ed0ee..ece01e73c 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -47,10 +47,10 @@ table {
           [ "gr_basic ( 𝐛❨?,?❩ )" * ]
           [ "gr_uni ( 𝐮❨?❩ )" "gr_uni_eq" * ]
           [ "gr_id ( 𝐢 ) " "gr_id_eq" * ]
-          [ "gr_tls ( ⫱*[?]? )" "gr_tls_eq" "gr_tls_pushs" "gr_tls_pushs_eq" "gr_tls_nexts_eq" * ]
+          [ "gr_tls ( â«°*[?]? )" "gr_tls_eq" "gr_tls_pushs" "gr_tls_pushs_eq" "gr_tls_nexts_eq" * ]
           [ "gr_nexts ( ↑*[?]? )" "gr_nexts_eq" * ]
           [ "gr_pushs ( ⫯*[?]? )" "gr_pushs_eq" * ]
-          [ "gr_tl ( ⫱? )" "gr_tl_eq" "gr_tl_eq_eq" * ]
+          [ "gr_tl ( â«°? )" "gr_tl_eq" "gr_tl_eq_eq" * ]
           [ "gr_eq ( ? ≡ ? )" * ]
           [ "gr_map ( ⫯? ) ( ↑? )" * ]
         }
@@ -118,8 +118,8 @@ table {
   class "yellow"
   [ { "extensions to the library" * } {
       [ { "streams" * } {
-          [ "stream_tls ( â«°*{?}[?]? )" "stream_tls_eq" * ]
-          [ "stream_hdtl ( â«°{?}? )" * ]
+          [ "stream_tls ( ⇣*{?}[?]? )" "stream_tls_eq" * ]
+          [ "stream_hdtl ( ⇣{?}? )" * ]
           [ "stream_eq ( ? ≗{?} ? )" "stream_eq_eq" * ]
           [ "stream ( ? ⨮{?} ? )" * ]
         }
diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops.ma
index d67deff75..407f8cc4f 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops.ma
@@ -419,12 +419,12 @@ qed-.
 (* Properties with application **********************************************)
 
 lemma drops_tls_at: ∀f,i1,i2. @❪i1,f❫ ≘ i2 →
-                    ∀b,L1,L2. ⇩*[b,⫱*[i2]f] L1 ≘ L2 →
-                    ⇩*[b,⫯⫱*[↑i2]f] L1 ≘ L2.
+                    ∀b,L1,L2. ⇩*[b,⫰*[i2]f] L1 ≘ L2 →
+                    ⇩*[b,⫯⫰*[↑i2]f] L1 ≘ L2.
 /3 width=3 by drops_eq_repl_fwd, at_inv_tls/ qed-.
 
 lemma drops_split_trans_bind2: ∀b,f,I,L,K0. ⇩*[b,f] L ≘ K0.ⓘ[I] → ∀i. @❪O,f❫ ≘ i →
-                               ∃∃J,K. ⇩[i]L ≘ K.ⓘ[J] & ⇩*[b,⫱*[↑i]f] K ≘ K0 & ⇧*[⫱*[↑i]f] I ≘ J.
+                               ∃∃J,K. ⇩[i]L ≘ K.ⓘ[J] & ⇩*[b,⫰*[↑i]f] K ≘ K0 & ⇧*[⫰*[↑i]f] I ≘ J.
 #b #f #I #L #K0 #H #i #Hf
 elim (drops_split_trans … H) -H [ |5: @(after_uni_dx … Hf) |2,3: skip ] /2 width=1 by after_isid_dx/ #Y #HLY #H
 lapply (drops_tls_at … Hf … H) -H #H
diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_sex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_sex.ma
index d9a9588a3..aeff28cee 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops_sex.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops_sex.ma
@@ -198,7 +198,7 @@ qed-.
 lemma sex_sdj_split_dx (R1) (R2) (RP):
       c_reflexive … R1 → c_reflexive … R2 → c_reflexive … RP →
       ∀L1,f1.
-      (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ↑g = ⫱*[n] f1 → R_pw_confluent1_sex R1 R1 R2 cfull g K I) →
+      (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ↑g = ⫰*[n] f1 → R_pw_confluent1_sex R1 R1 R2 cfull g K I) →
       ∀L2. L1 ⪤[R1,RP,f1] L2 → ∀f2. f1 ∥ f2 →
       ∃∃L. L1 ⪤[R2,cfull,f1] L & L ⪤[RP,R1,f2] L2.
 #R1 #R2 #RP #HR1 #HR2 #HRP #L1 elim L1 -L1
diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/seq.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/seq.ma
index f928bda7c..128cd2974 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/seq.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/seq.ma
@@ -110,7 +110,7 @@ lemma seq_inv_push (f):
 qed-.
 
 lemma seq_inv_tl (f):
-      ∀I,L1,L2. L1 ≡[⫱f] L2 → L1.ⓘ[I] ≡[f] L2.ⓘ[I].
+      ∀I,L1,L2. L1 ≡[⫰f] L2 → L1.ⓘ[I] ≡[f] L2.ⓘ[I].
 /2 width=1 by sex_inv_tl/ qed-.
 
 (* Basic_2A1: removed theorems 5:
diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma
index 72909212c..2a6946fca 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/sex.ma
@@ -177,7 +177,7 @@ lemma sex_inv_push (RN) (RP):
 qed-.
 
 lemma sex_inv_tl (RN) (RP):
-      ∀f,I1,I2,L1,L2. L1 ⪤[RN,RP,⫱f] L2 →
+      ∀f,I1,I2,L1,L2. L1 ⪤[RN,RP,⫰f] L2 →
       RN L1 I1 I2 → RP L1 I1 I2 →
       L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2].
 #RN #RP #f #I1 #I2 #L2 #L2 elim (pn_split f) *
@@ -188,7 +188,7 @@ qed-.
 
 lemma sex_fwd_bind (RN) (RP):
       ∀f,I1,I2,L1,L2.
-      L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] → L1 ⪤[RN,RP,⫱f] L2.
+      L1.ⓘ[I1] ⪤[RN,RP,f] L2.ⓘ[I2] → L1 ⪤[RN,RP,⫰f] L2.
 #RN #RP #f #I1 #I2 #L1 #L2 #Hf
 elim (pn_split f) * #g #H destruct
 [ elim (sex_inv_push … Hf) | elim (sex_inv_next … Hf) ] -Hf //
@@ -330,7 +330,7 @@ lemma sex_dec (RN) (RP):
   lapply (sex_inv_atom1 … H) -H #H destruct
 | #f @or_intror #H
   lapply (sex_inv_atom2 … H) -H #H destruct
-| #L2 #I2 #f elim (IH L2 (⫱f)) -IH #HL12
+| #L2 #I2 #f elim (IH L2 (â«°f)) -IH #HL12
   [2: /4 width=3 by sex_fwd_bind, or_intror/ ]
   elim (pn_split f) * #g #H destruct
   [ elim (HRP L1 I1 I2) | elim (HRN L1 I1 I2) ] -HRP -HRN #HV12
diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma
index 9d3e2df4d..a92cf28c1 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/sex_sex.ma
@@ -21,8 +21,8 @@ include "static_2/relocation/drops.ma".
 
 theorem sex_trans_gen (RN1) (RP1) (RN2) (RP2) (RN) (RP):
         ∀L1,f.
-        (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ↑g = ⫱*[n] f → R_pw_transitive_sex RN1 RN2 RN RN1 RP1 g K I) →
-        (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ⫯g = ⫱*[n] f → R_pw_transitive_sex RP1 RP2 RP RN1 RP1 g K I) →
+        (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ↑g = ⫰*[n] f → R_pw_transitive_sex RN1 RN2 RN RN1 RP1 g K I) →
+        (∀g,I,K,n. ⇩[n] L1 ≘ K.ⓘ[I] → ⫯g = ⫰*[n] f → R_pw_transitive_sex RP1 RP2 RP RN1 RP1 g K I) →
         ∀L0. L1 ⪤[RN1,RP1,f] L0 →
         ∀L2. L0 ⪤[RN2,RP2,f] L2 →
         L1 ⪤[RN,RP,f] L2.
@@ -64,8 +64,8 @@ qed-.
 
 theorem sex_conf (RN1) (RP1) (RN2) (RP2):
         ∀L,f.
-        (∀g,I,K,n. ⇩[n] L ≘ K.ⓘ[I] → ↑g = ⫱*[n] f → R_pw_confluent2_sex RN1 RN2 RN1 RP1 RN2 RP2 g K I) →
-        (∀g,I,K,n. ⇩[n] L ≘ K.ⓘ[I] → ⫯g = ⫱*[n] f → R_pw_confluent2_sex RP1 RP2 RN1 RP1 RN2 RP2 g K I) →
+        (∀g,I,K,n. ⇩[n] L ≘ K.ⓘ[I] → ↑g = ⫰*[n] f → R_pw_confluent2_sex RN1 RN2 RN1 RP1 RN2 RP2 g K I) →
+        (∀g,I,K,n. ⇩[n] L ≘ K.ⓘ[I] → ⫯g = ⫰*[n] f → R_pw_confluent2_sex RP1 RP2 RN1 RP1 RN2 RP2 g K I) →
         pw_confluent2 … (sex RN1 RP1 f) (sex RN2 RP2 f) L.
 #RN1 #RP1 #RN2 #RP2 #L elim L -L
 [ #f #_ #_ #L1 #H1 #L2 #H2 >(sex_inv_atom1 … H1) >(sex_inv_atom1 … H2) -H2 -H1
@@ -85,8 +85,8 @@ theorem sex_conf (RN1) (RP1) (RN2) (RP2):
 qed-.
 
 lemma sex_repl (RN) (RP) (SN) (SP) (L1) (f):
-      (∀g,I,K1,n. ⇩[n] L1 ≘ K1.ⓘ[I] → ↑g = ⫱*[n] f → R_pw_replace3_sex … RN SN RN RP SN SP g K1 I) →
-      (∀g,I,K1,n. ⇩[n] L1 ≘ K1.ⓘ[I] → ⫯g = ⫱*[n] f → R_pw_replace3_sex … RP SP RN RP SN SP g K1 I) →
+      (∀g,I,K1,n. ⇩[n] L1 ≘ K1.ⓘ[I] → ↑g = ⫰*[n] f → R_pw_replace3_sex … RN SN RN RP SN SP g K1 I) →
+      (∀g,I,K1,n. ⇩[n] L1 ≘ K1.ⓘ[I] → ⫯g = ⫰*[n] f → R_pw_replace3_sex … RP SP RN RP SN SP g K1 I) →
       ∀L2. L1 ⪤[RN,RP,f] L2 → ∀K1. L1 ⪤[SN,SP,f] K1 →
       ∀K2. L2 ⪤[SN,SP,f] K2 → K1 ⪤[RN,RP,f] K2.
 #RN #RP #SN #SP #L1 elim L1 -L1
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/frees.ma b/matita/matita/contribs/lambdadelta/static_2/static/frees.ma
index 887703487..e9e6380d4 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/frees.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/frees.ma
@@ -28,7 +28,7 @@ inductive frees: relation3 lenv term rtmap ≝
               frees (L.ⓘ[I]) (#↑i) (⫯f)
 | frees_gref: ∀f,L,l. 𝐈❪f❫ → frees L (§l) f
 | frees_bind: ∀f1,f2,f,p,I,L,V,T. frees L V f1 → frees (L.ⓑ[I]V) T f2 →
-              f1 ⋓ ⫱f2 ≘ f → frees L (ⓑ[p,I]V.T) f
+              f1 ⋓ ⫰f2 ≘ f → frees L (ⓑ[p,I]V.T) f
 | frees_flat: ∀f1,f2,f,I,L,V,T. frees L V f1 → frees L T f2 →
               f1 ⋓ f2 ≘ f → frees L (ⓕ[I]V.T) f
 .
@@ -143,7 +143,7 @@ lemma frees_inv_gref: ∀f,L,l. L ⊢ 𝐅+❪§l❫ ≘ f → 𝐈❪f❫.
 
 fact frees_inv_bind_aux:
      ∀f,L,X. L ⊢ 𝐅+❪X❫ ≘ f → ∀p,I,V,T. X = ⓑ[p,I]V.T →
-     ∃∃f1,f2. L ⊢ 𝐅+❪V❫ ≘ f1 & L.ⓑ[I]V ⊢ 𝐅+❪T❫ ≘ f2 & f1 ⋓ ⫱f2 ≘ f.
+     ∃∃f1,f2. L ⊢ 𝐅+❪V❫ ≘ f1 & L.ⓑ[I]V ⊢ 𝐅+❪T❫ ≘ f2 & f1 ⋓ ⫰f2 ≘ f.
 #f #L #X * -f -L -X
 [ #f #L #s #_ #q #J #W #U #H destruct
 | #f #i #_ #q #J #W #U #H destruct
@@ -158,7 +158,7 @@ qed-.
 
 lemma frees_inv_bind:
       ∀f,p,I,L,V,T. L ⊢ 𝐅+❪ⓑ[p,I]V.T❫ ≘ f →
-      ∃∃f1,f2. L ⊢ 𝐅+❪V❫ ≘ f1 & L.ⓑ[I]V ⊢ 𝐅+❪T❫ ≘ f2 & f1 ⋓ ⫱f2 ≘ f.
+      ∃∃f1,f2. L ⊢ 𝐅+❪V❫ ≘ f1 & L.ⓑ[I]V ⊢ 𝐅+❪T❫ ≘ f2 & f1 ⋓ ⫰f2 ≘ f.
 /2 width=4 by frees_inv_bind_aux/ qed-.
 
 fact frees_inv_flat_aux: ∀f,L,X. L ⊢ 𝐅+❪X❫ ≘ f → ∀I,V,T. X = ⓕ[I]V.T →
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma
index 7b4f04950..69e0158e9 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/frees_drops.ma
@@ -171,7 +171,7 @@ qed-.
 lemma frees_inv_lifts_SO:
       ∀b,f,L,U. L ⊢ 𝐅+❪U❫ ≘ f →
       ∀K. ⇩*[b,𝐔❨1❩] L ≘ K → ∀T. ⇧[1] T ≘ U →
-      K ⊢ 𝐅+❪T❫ ≘ ⫱f.
+      K ⊢ 𝐅+❪T❫ ≘ ⫰f.
 #b #f #L #U #H #K #HLK #T #HTU elim(frees_inv_lifts_ex … H … HLK … HTU) -b -L -U
 #f1 #Hf #Hf1 elim (coafter_inv_nxx … Hf) -Hf
 /3 width=5 by frees_eq_repl_back, coafter_isid_inv_sn/
@@ -189,7 +189,7 @@ qed-.
 lemma frees_inv_drops_next:
       ∀f1,L1,T1. L1 ⊢ 𝐅+❪T1❫ ≘ f1 →
       ∀I2,L2,V2,i. ⇩[i] L1 ≘ L2.ⓑ[I2]V2 →
-      ∀g1. ↑g1 = ⫱*[i] f1 →
+      ∀g1. ↑g1 = ⫰*[i] f1 →
       ∃∃g2. L2 ⊢ 𝐅+❪V2❫ ≘ g2 & g2 ⊆ g1.
 #f1 #L1 #T1 #H elim H -f1 -L1 -T1
 [ #f1 #L1 #s #Hf1 #I2 #L2 #V2 #j #_ #g1 #H1 -I2 -L1 -s
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma b/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma
index 05500252c..0ae38b461 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/frees_fqup.ma
@@ -39,7 +39,7 @@ lemma frees_total: ∀L,T. ∃f. L ⊢ 𝐅+❪T❫ ≘ f.
 | #p #I #V #T #HG #HL #HT destruct
   elim (IH G L V) // #f1 #HV
   elim (IH G (L.ⓑ[I]V) T) -IH // #f2 #HT
-  elim (sor_isfin_ex f1 (⫱f2))
+  elim (sor_isfin_ex f1 (â«°f2))
   /3 width=6 by frees_fwd_isfin, frees_bind, isfin_tl, ex_intro/
 | #I #V #T #HG #HL #HT destruct
   elim (IH G L V) // #f1 #HV
@@ -53,7 +53,7 @@ qed-.
 
 theorem frees_bind_void:
         ∀f1,L,V. L ⊢ 𝐅+❪V❫ ≘ f1 → ∀f2,T. L.ⓧ ⊢ 𝐅+❪T❫ ≘ f2 →
-        ∀f. f1 ⋓ ⫱f2 ≘ f → ∀p,I. L ⊢ 𝐅+❪ⓑ[p,I]V.T❫ ≘ f.
+        ∀f. f1 ⋓ ⫰f2 ≘ f → ∀p,I. L ⊢ 𝐅+❪ⓑ[p,I]V.T❫ ≘ f.
 #f1 #L #V #Hf1 #f2 #T #Hf2 #f #Hf #p #I
 elim (frees_total (L.ⓑ[I]V) T) #f0 #Hf0
 lapply (lsubr_lsubf … Hf2 … Hf0) -Hf2 /2 width=5 by lsubr_unit/ #H02
@@ -81,7 +81,7 @@ qed-.
 
 lemma frees_inv_bind_void:
       ∀f,p,I,L,V,T. L ⊢ 𝐅+❪ⓑ[p,I]V.T❫ ≘ f →
-      ∃∃f1,f2. L ⊢ 𝐅+❪V❫ ≘ f1 & L.ⓧ ⊢ 𝐅+❪T❫ ≘ f2 & f1 ⋓ ⫱f2 ≘ f.
+      ∃∃f1,f2. L ⊢ 𝐅+❪V❫ ≘ f1 & L.ⓧ ⊢ 𝐅+❪T❫ ≘ f2 & f1 ⋓ ⫰f2 ≘ f.
 #f #p #I #L #V #T #H
 elim (frees_inv_bind … H) -H #f1 #f2 #Hf1 #Hf2 #Hf
 elim (frees_total (L.ⓧ) T) #f0 #Hf0
@@ -119,7 +119,7 @@ lemma frees_ind_void (Q:relation3 …):
         ∀f,L,l. 𝐈❪f❫ →  Q L (§l) f
       ) → (
         ∀f1,f2,f,p,I,L,V,T.
-        L ⊢ 𝐅+❪V❫ ≘ f1 → L.ⓧ ⊢𝐅+❪T❫≘ f2 → f1 ⋓ ⫱f2 ≘ f →
+        L ⊢ 𝐅+❪V❫ ≘ f1 → L.ⓧ ⊢𝐅+❪T❫≘ f2 → f1 ⋓ ⫰f2 ≘ f →
         Q L V f1 → Q (L.ⓧ) T f2 → Q L (ⓑ[p,I]V.T) f
       ) → (
         ∀f1,f2,f,I,L,V,T.
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/fsle.ma b/matita/matita/contribs/lambdadelta/static_2/static/fsle.ma
index 191612548..659060756 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/fsle.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/fsle.ma
@@ -22,7 +22,7 @@ include "static_2/static/frees.ma".
 
 definition fsle: bi_relation lenv term ≝ λL1,T1,L2,T2.
                  ∃∃n1,n2,f1,f2. L1 ⊢ 𝐅+❪T1❫ ≘ f1 & L2 ⊢ 𝐅+❪T2❫ ≘ f2 &
-                                L1 ≋ⓧ*[n1,n2] L2 & ⫱*[n1]f1 ⊆ ⫱*[n2]f2.
+                                L1 ≋ⓧ*[n1,n2] L2 & ⫰*[n1]f1 ⊆ ⫰*[n2]f2.
 
 interpretation "free variables inclusion (restricted closure)"
    'SubSetEq L1 T1 L2 T2 = (fsle L1 T1 L2 T2).
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/fsle_drops.ma b/matita/matita/contribs/lambdadelta/static_2/static/fsle_drops.ma
index 110e0fd08..718a74a8a 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/fsle_drops.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/fsle_drops.ma
@@ -68,7 +68,7 @@ lemma fsle_inv_lifts_sn: ∀T1,U1. ⇧[1] T1 ≘ U1 →
 * #n #m #f2 #g2 #Hf2 #Hg2 #HL #Hfg2 #p
 elim (lveq_inv_pair_pair … HL) -HL #HL #H1 #H2 destruct
 elim (frees_total L2 V2) #g1 #Hg1
-elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+elim (sor_isfin_ex g1 (â«°g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
 lapply (frees_inv_lifts_SO (Ⓣ) … Hf2 … HTU1)
 [1,2: /3 width=4 by drops_refl, drops_drop/ ] -U1 #Hf2
 lapply (sor_inv_sle_dx … Hg) #H0g
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/fsle_fqup.ma b/matita/matita/contribs/lambdadelta/static_2/static/fsle_fqup.ma
index 242c3d52c..7965876e2 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/fsle_fqup.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/fsle_fqup.ma
@@ -33,7 +33,7 @@ lemma fsle_shift: ∀L1,L2. |L1| = |L2| →
 elim (lveq_inj_length … H2L) // -H1L #H1 #H2 destruct
 lapply (lveq_inv_bind_O … H2L) -H2L #HL
 elim (frees_total L2 V) #g1 #Hg1
-elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+elim (sor_isfin_ex g1 (â«°g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
 lapply (sor_inv_sle_dx … Hg) #H0g
 /4 width=10 by frees_bind, lveq_void_sn, sle_tl, sle_trans, ex4_4_intro/
 qed.
@@ -42,7 +42,7 @@ lemma fsle_bind_dx_sn: ∀L1,L2,V1,V2. ❪L1,V1❫ ⊆ ❪L2,V2❫ →
                        ∀p,I,T2. ❪L1,V1❫ ⊆ ❪L2,ⓑ[p,I]V2.T2❫.
 #L1 #L2 #V1 #V2 * #n1 #m1 #f1 #g1 #Hf1 #Hg1 #HL12 #Hfg1 #p #I #T2
 elim (frees_total (L2.ⓧ) T2) #g2 #Hg2
-elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+elim (sor_isfin_ex g1 (â«°g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
 @(ex4_4_intro … g Hf1 … HL12) (**) (* full auto too slow *)
 /4 width=5 by frees_bind_void, sor_inv_sle_sn, sor_tls, sle_trans/
 qed.
@@ -53,7 +53,7 @@ lemma fsle_bind_dx_dx: ∀L1,L2,T1,T2. ❪L1,T1❫ ⊆ ❪L2.ⓧ,T2❫ → |L1|
 elim (lveq_inv_void_dx_length … H HL12) -H -HL12 #m1 #HL12 #H1 #H2 destruct
 <tls_xn in Hfg2; #Hfg2
 elim (frees_total L2 V2) #g1 #Hg1
-elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+elim (sor_isfin_ex g1 (â«°g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
 @(ex4_4_intro … g Hf2 … HL12) (**) (* full auto too slow *)
 /4 width=5 by frees_bind_void, sor_inv_sle_dx, sor_tls, sle_trans/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/fsle_fsle.ma b/matita/matita/contribs/lambdadelta/static_2/static/fsle_fsle.ma
index abbee2fdc..e9ebfb381 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/fsle_fsle.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/fsle_fsle.ma
@@ -22,7 +22,7 @@ include "static_2/static/fsle_fqup.ma".
 lemma fsle_frees_trans:
       ∀L1,L2,T1,T2. ❪L1,T1❫ ⊆ ❪L2,T2❫ →
       ∀f2. L2 ⊢ 𝐅+❪T2❫ ≘ f2 →
-      ∃∃n1,n2,f1. L1 ⊢ 𝐅+❪T1❫ ≘ f1 & L1 ≋ⓧ*[n1,n2] L2 & ⫱*[n1]f1 ⊆ ⫱*[n2]f2.
+      ∃∃n1,n2,f1. L1 ⊢ 𝐅+❪T1❫ ≘ f1 & L1 ≋ⓧ*[n1,n2] L2 & ⫰*[n1]f1 ⊆ ⫰*[n2]f2.
 #L1 #L2 #T1 #T2 * #n1 #n2 #f1 #g2 #Hf1 #Hg2 #HL #Hn #f2 #Hf2
 lapply (frees_mono … Hg2 … Hf2) -Hg2 -Hf2 #Hgf2
 lapply (tls_eq_repl n2 … Hgf2) -Hgf2 #Hgf2
@@ -53,7 +53,7 @@ qed-.
 lemma fsle_frees_conf:
       ∀L1,L2,T1,T2. ❪L1,T1❫ ⊆ ❪L2,T2❫ →
       ∀f1. L1 ⊢ 𝐅+❪T1❫ ≘ f1 →
-      ∃∃n1,n2,f2. L2 ⊢ 𝐅+❪T2❫ ≘ f2 & L1 ≋ⓧ*[n1,n2] L2 & ⫱*[n1]f1 ⊆ ⫱*[n2]f2.
+      ∃∃n1,n2,f2. L2 ⊢ 𝐅+❪T2❫ ≘ f2 & L1 ≋ⓧ*[n1,n2] L2 & ⫰*[n1]f1 ⊆ ⫰*[n2]f2.
 #L1 #L2 #T1 #T2 * #n1 #n2 #g1 #g2 #Hg1 #Hg2 #HL #Hn #f1 #Hf1
 lapply (frees_mono … Hg1 … Hf1) -Hg1 -Hf1 #Hgf1
 lapply (tls_eq_repl n1 … Hgf1) -Hgf1 #Hgf1
@@ -120,7 +120,7 @@ theorem fsle_bind_sn_ge:
 #L1 #L2 #HL #V1 #T1 #T * #n1 #x #f1 #g #Hf1 #Hg #H1n1 #H2n1 #H #p #I
 elim (fsle_frees_trans … H … Hg) -H #n2 #n #f2 #Hf2 #H1n2 #H2n2
 elim (lveq_inj_void_sn_ge … H1n1 … H1n2) -H1n2 // #H1 #H2 #H3 destruct
-elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
+elim (sor_isfin_ex f1 (â«°f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
 <tls_xn in H2n2; #H2n2
 /4 width=12 by frees_bind_void, sor_inv_sle, sor_tls, ex4_4_intro/
 qed.
@@ -144,8 +144,8 @@ theorem fsle_bind_eq:
 * #n2 #m2 #f2 #g2 #Hf2 #Hg2 #H2L #Hfg2 #p #I1
 elim (lveq_inj_length … H1L) // #H1 #H2 destruct
 elim (lveq_inj_length … H2L) // -HL -H2L #H1 #H2 destruct
-elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
-elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+elim (sor_isfin_ex f1 (â«°f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
+elim (sor_isfin_ex g1 (â«°g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
 /4 width=15 by frees_bind_void, frees_bind, monotonic_sle_sor, sle_tl, ex4_4_intro/
 qed.
 
@@ -158,8 +158,8 @@ theorem fsle_bind:
 * #n2 #m2 #f2 #g2 #Hf2 #Hg2 #H2L #Hfg2 #p
 elim (lveq_inv_pair_pair … H2L) -H2L #H2L #H1 #H2 destruct
 elim (lveq_inj … H2L … H1L) -H1L #H1 #H2 destruct
-elim (sor_isfin_ex f1 (⫱f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
-elim (sor_isfin_ex g1 (⫱g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
+elim (sor_isfin_ex f1 (â«°f2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #f #Hf #_
+elim (sor_isfin_ex g1 (â«°g2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #g #Hg #_
 /4 width=15 by frees_bind, monotonic_sle_sor, sle_tl, ex4_4_intro/
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma b/matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma
index 95cec9a87..8e63f58d2 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/lsubf.ma
@@ -270,7 +270,7 @@ qed-.
 (* Basic forward lemmas *****************************************************)
 
 lemma lsubf_fwd_bind_tl:
-      ∀f1,f2,I,L1,L2. ❪L1.ⓘ[I],f1❫ ⫃𝐅+ ❪L2.ⓘ[I],f2❫ → ❪L1,⫱f1❫ ⫃𝐅+ ❪L2,⫱f2❫.
+      ∀f1,f2,I,L1,L2. ❪L1.ⓘ[I],f1❫ ⫃𝐅+ ❪L2.ⓘ[I],f2❫ → ❪L1,⫰f1❫ ⫃𝐅+ ❪L2,⫰f2❫.
 #f1 #f2 #I #L1 #L2 #H
 elim (pn_split f1) * #g1 #H0 destruct
 [ elim (lsubf_inv_push_sn … H) | elim (lsubf_inv_bind_sn … H) ] -H
@@ -360,8 +360,8 @@ lemma lsubf_refl_eq: ∀f1,f2,L. f1 ≡ f2 → ❪L,f1❫ ⫃𝐅+ ❪L,f2❫.
 /2 width=3 by lsubf_eq_repl_back2/ qed.
 
 lemma lsubf_bind_tl_dx:
-      ∀g1,f2,I,L1,L2. ❪L1,g1❫ ⫃𝐅+ ❪L2,⫱f2❫ →
-      ∃∃f1. ❪L1.ⓘ[I],f1❫ ⫃𝐅+ ❪L2.ⓘ[I],f2❫ & g1 = ⫱f1.
+      ∀g1,f2,I,L1,L2. ❪L1,g1❫ ⫃𝐅+ ❪L2,⫰f2❫ →
+      ∃∃f1. ❪L1.ⓘ[I],f1❫ ⫃𝐅+ ❪L2.ⓘ[I],f2❫ & g1 = ⫰f1.
 #g1 #f2 #I #L1 #L2 #H
 elim (pn_split f2) * #g2 #H2 destruct
 @ex2_intro [1,2,4,5: /2 width=2 by lsubf_push, lsubf_bind/ ] // (**) (* constructor needed *)
@@ -369,8 +369,8 @@ qed-.
 
 lemma lsubf_beta_tl_dx:
       ∀f,f0,g1,L1,V. L1 ⊢ 𝐅+❪V❫ ≘ f → f0 ⋓ f ≘ g1 →
-      ∀f2,L2,W. ❪L1,f0❫ ⫃𝐅+ ❪L2,⫱f2❫ →
-      ∃∃f1. ❪L1.ⓓⓝW.V,f1❫ ⫃𝐅+ ❪L2.ⓛW,f2❫ & ⫱f1 ⊆ g1.
+      ∀f2,L2,W. ❪L1,f0❫ ⫃𝐅+ ❪L2,⫰f2❫ →
+      ∃∃f1. ❪L1.ⓓⓝW.V,f1❫ ⫃𝐅+ ❪L2.ⓛW,f2❫ & ⫰f1 ⊆ g1.
 #f #f0 #g1 #L1 #V #Hf #Hg1 #f2
 elim (pn_split f2) * #x2 #H2 #L2 #W #HL12 destruct
 [ /3 width=4 by lsubf_push, sor_inv_sle_sn, ex2_intro/
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rex_drops.ma b/matita/matita/contribs/lambdadelta/static_2/static/rex_drops.ma
index dba0cb30b..b6374ac0b 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/rex_drops.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/rex_drops.ma
@@ -40,12 +40,12 @@ definition f_dropable_dx:
 definition f_transitive_next:
            relation3 … ≝ λR1,R2,R3.
            ∀f,L,T. L ⊢ 𝐅+❪T❫ ≘ f →
-           ∀g,I,K,i. ⇩[i] L ≘ K.ⓘ[I] → ↑g = ⫱*[i] f →
+           ∀g,I,K,i. ⇩[i] L ≘ K.ⓘ[I] → ↑g = ⫰*[i] f →
            R_pw_transitive_sex (cext2 R1) (cext2 R2) (cext2 R3) (cext2 R1) cfull g K I.
 
 definition f_confluent1_next: relation2 … ≝ λR1,R2.
            ∀f,L,T. L ⊢ 𝐅+❪T❫ ≘ f →
-           ∀g,I,K,i. ⇩[i] L ≘ K.ⓘ[I] → ↑g = ⫱*[i] f →
+           ∀g,I,K,i. ⇩[i] L ≘ K.ⓘ[I] → ↑g = ⫰*[i] f →
            R_pw_confluent1_sex (cext2 R1) (cext2 R1) (cext2 R2) cfull g K I.
 
 (* Properties with generic slicing for local environments *******************)
diff --git a/matita/matita/contribs/lambdadelta/static_2/static/rex_rex.ma b/matita/matita/contribs/lambdadelta/static_2/static/rex_rex.ma
index 5604348bf..ba250697a 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/rex_rex.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/rex_rex.ma
@@ -45,7 +45,7 @@ theorem rex_bind (R) (p) (I):
         ∀L1,L2,V1,V2,T. L1 ⪤[R,V1] L2 → L1.ⓑ[I]V1 ⪤[R,T] L2.ⓑ[I]V2 →
         L1 ⪤[R,ⓑ[p,I]V1.T] L2.
 #R #p #I #L1 #L2 #V1 #V2 #T * #f1 #HV #Hf1 * #f2 #HT #Hf2
-lapply (sex_fwd_bind … Hf2) -Hf2 #Hf2 elim (sor_isfin_ex f1 (⫱f2))
+lapply (sex_fwd_bind … Hf2) -Hf2 #Hf2 elim (sor_isfin_ex f1 (⫰f2))
 /3 width=7 by frees_fwd_isfin, frees_bind, sex_join, isfin_tl, ex2_intro/
 qed.
 
@@ -59,7 +59,7 @@ qed.
 theorem rex_bind_void (R) (p) (I):
         ∀L1,L2,V,T. L1 ⪤[R,V] L2 → L1.ⓧ ⪤[R,T] L2.ⓧ → L1 ⪤[R,ⓑ[p,I]V.T] L2.
 #R #p #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2
-lapply (sex_fwd_bind … Hf2) -Hf2 #Hf2 elim (sor_isfin_ex f1 (⫱f2))
+lapply (sex_fwd_bind … Hf2) -Hf2 #Hf2 elim (sor_isfin_ex f1 (⫰f2))
 /3 width=7 by frees_fwd_isfin, frees_bind_void, sex_join, isfin_tl, ex2_intro/
 qed.
 
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 09bcabd57..671b2b031 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1521,7 +1521,7 @@ let predefined_classes = [
  ["⇕"; "⇳"; "⬍"; "↕"; ];
  ["↔"; "⇔"; "⬄"; "⬌"; ] ; 
  ["≤"; "≲"; "≼"; "≰"; "≴"; "⋠"; "⊆"; "⫃"; "⊑"; ] ;
- ["_"; "↓"; "↙"; "⎽"; "⎼"; "⎻"; "⎺"; ];
+ ["_"; "↓"; "↙"; "⇣"; "⎽"; "⎼"; "⎻"; "⎺"; ];
  ["<"; "≺"; "≮"; "⊀"; "〈"; "«"; "❬"; "❮"; "❰"; ] ;
  ["("; "❨"; "❪"; "❲"; "（"; ];
  [")"; "❩"; "❫"; "❳"; "）"; ];
-- 
2.39.2