From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 19 May 2022 10:11:11 +0000 (+0200)
Subject: update in ground
X-Git-Tag: make_still_working~71
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=77479649510792efe4d9cbff508e118360862594;p=helm.git

update in ground

+ new notation for application of a relocation
---

diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/flifts.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/flifts.ma
index 9a5db82f1..e015813b0 100644
--- a/matita/matita/contribs/lambdadelta/apps_2/functional/flifts.ma
+++ b/matita/matita/contribs/lambdadelta/apps_2/functional/flifts.ma
@@ -21,7 +21,7 @@ include "static_2/relocation/lifts.ma".
 rec definition flifts f U on U ≝ match U with
 [ TAtom I     ⇒ match I with
   [ Sort _ ⇒ U
-  | LRef i ⇒ #(f@❨i❩)
+  | LRef i ⇒ #(f＠⧣❨i❩)
   | GRef _ ⇒ U
   ]
 | TPair I V T ⇒ match I with
@@ -38,7 +38,7 @@ interpretation "uniform functional relocation (term)"
 
 (* Basic properties *********************************************************)
 
-lemma flifts_lref (f) (i): ↑*[f](#i) = #(f@❨i❩).
+lemma flifts_lref (f) (i): ↑*[f](#i) = #(f＠⧣❨i❩).
 // qed.
 
 lemma flifts_bind (f) (p) (I) (V) (T): ↑*[f](ⓑ[p,I]V.T) = ⓑ[p,I]↑*[f]V.↑*[⫯f]T.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma
index f17d53ff8..9eac0d04c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/at_2.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR DELAYED UPDATING ********************************************)
 
-notation "hvbox( @ break term 71 u . break term 70 t )"
+notation "hvbox( ï¼  break term 71 u . break term 70 t )"
   non associative with precedence 70
   for @{ 'At $u $t }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
index 849c5f32d..b7f900b6c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
@@ -28,7 +28,7 @@ include "ground/xoa/and_4.ma".
 definition dfr (p) (q): relation2 prototerm prototerm ≝
            λt1,t2. ∃∃b,n.
            let r ≝ p●𝗔◗b●𝗟◗q in
-           ∧∧ (⊗b ϵ 𝐁 ∧ 𝟎 = ♭b) & ↑♭q = (▼[r]𝐢)@❨n❩ & r◖𝗱n ϵ t1 &
+           ∧∧ (⊗b ϵ 𝐁 ∧ 𝟎 = ♭b) & ↑♭q = (▼[r]𝐢)＠⧣❨n❩ & r◖𝗱n ϵ t1 &
               t1[⋔r←𝛗(n+♭b).(t1⋔(p◖𝗦))] ⇔ t2
 .
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
index 2d3fdbdf5..29c44898d 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -32,11 +32,11 @@ include "ground/relocation/tr_pap_pushs.ma".
 
 (* COMMENT
 axiom pippo (b) (q) (n):
-      ↑❘q❘ = (↑[q]𝐢)@❨n❩ →
-      ↑❘q❘+❘b❘= (↑[b●𝗟◗q]𝐢)@❨n+❘b❘❩.
+      ↑❘q❘ = (↑[q]𝐢)＠⧣❨n❩ →
+      ↑❘q❘+❘b❘= (↑[b●𝗟◗q]𝐢)＠⧣❨n+❘b❘❩.
 
 lemma unwind_rmap_tls_eq_id (p) (n):
-      ❘p❘ = ↑[p]𝐢@❨n❩ →
+      ❘p❘ = ↑[p]𝐢＠⧣❨n❩ →
       (𝐢) ≗ ⇂*[n]↑[p]𝐢.
 #p @(list_ind_rcons … p) -p
 [ #n <depth_empty #H destruct
@@ -56,10 +56,10 @@ lemma unwind_rmap_tls_eq_id (p) (n):
 ]
 
 
-(*  (↑❘q❘+❘b❘=↑[b●𝗟◗q]𝐢@❨n+❘b❘❩ *)
-(* [↑[p]𝐢@❨n❩]⫯*[❘p❘]f∘⇂*[n]↑[p]𝐢) *)
+(*  (↑❘q❘+❘b❘=↑[b●𝗟◗q]𝐢＠⧣❨n+❘b❘❩ *)
+(* [↑[p]𝐢＠⧣❨n❩]⫯*[❘p❘]f∘⇂*[n]↑[p]𝐢) *)
 lemma unwind_rmap_tls_eq (f) (p) (n):
-      ❘p❘ = ↑[p]𝐢@❨n❩ →
+      ❘p❘ = ↑[p]𝐢＠⧣❨n❩ →
       f ≗ ⇂*[n]↑[p]f.
 #f #p #n #Hp
 @(stream_eq_canc_dx … (stream_tls_eq_repl …))
@@ -124,9 +124,9 @@ lemma dfr_unwind_id_bi (p) (q) (t1) (t2): t1 ϵ 𝐓 →
 ]
 
 (*
-Hn : ↑❘q❘ = ↑[p●𝗔◗b●𝗟◗q]𝐢@❨n❩
+Hn : ↑❘q❘ = ↑[p●𝗔◗b●𝗟◗q]𝐢＠⧣❨n❩
 ---------------------------
-↑[𝐮❨↑❘q❘+❘b❘❩] ↑[↑[p]𝐢] t ⇔ ↑[𝐮❨↑[p●𝗔◗b●𝗟◗q]𝐢@❨n+❘b❘❩❩] t
+↑[𝐮❨↑❘q❘+❘b❘❩] ↑[↑[p]𝐢] t ⇔ ↑[𝐮❨↑[p●𝗔◗b●𝗟◗q]𝐢＠⧣❨n+❘b❘❩❩] t
 *)
 (*
 (↑[𝐮❨↑❘q❘❩]▼[⇂*[↑❘q❘]▼[p●𝗟◗q]𝐢](t1⋔(p◖𝗦))⇔▼[𝐮❨↑❘q❘❩∘▼[p●𝗔◗b●𝗟◗q]𝐢](t1⋔(p◖𝗦))
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
index d2a33afc2..6c7be675a 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
@@ -28,7 +28,7 @@ include "ground/xoa/and_4.ma".
 definition ifr (p) (q): relation2 prototerm prototerm ≝
            λt1,t2. ∃∃b,n.
            let r ≝ p●𝗔◗b●𝗟◗q in
-           ∧∧ (⊗b ϵ 𝐁 ∧ 𝟎 = ♭b) & ↑♭q = (▼[r]𝐢)@❨n❩ & r◖𝗱n ϵ t1 &
+           ∧∧ (⊗b ϵ 𝐁 ∧ 𝟎 = ♭b) & ↑♭q = (▼[r]𝐢)＠⧣❨n❩ & r◖𝗱n ϵ t1 &
               t1[⋔r←↑[𝐮❨♭(b●𝗟◗q)❩](t1⋔(p◖𝗦))] ⇔ t2
 .
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
index a487fcf5a..ec7d9726f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
@@ -28,7 +28,7 @@ match p with
 [ list_empty     ⇒ k f (𝐞)
 | list_lcons l q ⇒
   match l with
-  [ label_d n ⇒ lift_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (⇂*[n]f) q
+  [ label_d n ⇒ lift_gen (A) (λg,p. k g (𝗱(f＠⧣❨n❩)◗p)) (⇂*[n]f) q
   | label_m   ⇒ lift_gen (A) (λg,p. k g (𝗺◗p)) f q
   | label_L   ⇒ lift_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q
   | label_A   ⇒ lift_gen (A) (λg,p. k g (𝗔◗p)) f q
@@ -61,7 +61,7 @@ lemma lift_empty (A) (k) (f):
 // qed.
 
 lemma lift_d_sn (A) (k) (p) (n) (f):
-      ↑❨(λg,p. k g (𝗱(f@❨n❩)◗p)), ⇂*[n]f, p❩ = ↑{A}❨k, f, 𝗱n◗p❩.
+      ↑❨(λg,p. k g (𝗱(f＠⧣❨n❩)◗p)), ⇂*[n]f, p❩ = ↑{A}❨k, f, 𝗱n◗p❩.
 // qed.
 
 lemma lift_m_sn (A) (k) (p) (f):
@@ -146,5 +146,5 @@ lemma lift_rmap_S_dx (f) (p):
 // qed.
 
 lemma lift_rmap_pap_d_dx (f) (p) (n) (m):
-      ↑[p]f@❨m+n❩ = ↑[p◖𝗱n]f@❨m❩+↑[p]f@❨n❩.
+      ↑[p]f＠⧣❨m+n❩ = ↑[p◖𝗱n]f＠⧣❨m❩+↑[p]f＠⧣❨n❩.
 // qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
index 772c837fb..06e03b13a 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
@@ -24,21 +24,21 @@ lemma lift_iref_bi (t1) (t2) (n):
 qed.
 
 lemma lift_iref_sn (f) (t:prototerm) (n:pnat):
-      (𝛗f@❨n❩.↑[⇂*[n]f]t) ⊆ ↑[f](𝛗n.t).
+      (𝛗f＠⧣❨n❩.↑[⇂*[n]f]t) ⊆ ↑[f](𝛗n.t).
 #f #t #n #p * #q * #r #Hr #H1 #H2 destruct
 @(ex2_intro … (𝗱n◗𝗺◗r))
 /2 width=1 by in_comp_iref/
 qed-.
 
 lemma lift_iref_dx (f) (t) (n:pnat):
-      ↑[f](𝛗n.t) ⊆ 𝛗f@❨n❩.↑[⇂*[n]f]t.
+      ↑[f](𝛗n.t) ⊆ 𝛗f＠⧣❨n❩.↑[⇂*[n]f]t.
 #f #t #n #p * #q #Hq #H0 destruct
 elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct
 /3 width=1 by in_comp_iref, in_comp_lift_bi/
 qed-.
 
 lemma lift_iref (f) (t) (n:pnat):
-      (𝛗f@❨n❩.↑[⇂*[n]f]t) ⇔ ↑[f](𝛗n.t).
+      (𝛗f＠⧣❨n❩.↑[⇂*[n]f]t) ⇔ ↑[f](𝛗n.t).
 /3 width=1 by conj, lift_iref_sn, lift_iref_dx/
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
index fad4995de..68a4ceb36 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
@@ -92,7 +92,7 @@ lemma lift_path_lcons (f) (p) (l):
 qed.
 
 lemma lift_path_d_sn (f) (p) (n):
-      (𝗱(f@❨n❩)◗↑[⇂*[n]f]p) = ↑[f](𝗱n◗p).
+      (𝗱(f＠⧣❨n❩)◗↑[⇂*[n]f]p) = ↑[f](𝗱n◗p).
 // qed.
 
 lemma lift_path_m_sn (f) (p):
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/nap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/nap.ma
index 502765a0a..bfa89a784 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/nap.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/nap.ma
@@ -13,14 +13,14 @@ lemma nlt_npsucc_bi (n1) (n2):
 qed.
 
 definition tr_nap (f) (l:nat): nat ≝
-           ↓(f@❨↑l❩).
+           ↓(f＠⧣❨↑l❩).
 
 interpretation
   "functional non-negative application (total relocation maps)"
   'ApplySucc f l = (tr_nap f l).
 
 lemma tr_nap_unfold (f) (l):
-      ↓(f@❨↑l❩) = f@↑❨l❩.
+      ↓(f＠⧣❨↑l❩) = f@↑❨l❩.
 // qed.
 
 lemma tr_compose_nap (f2) (f1) (l):
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma
index bff50807d..6eb8b3ae8 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma
@@ -25,7 +25,7 @@ match p with
   match l with
   [ label_d n ⇒
     match q with
-    [ list_empty     ⇒ 𝗱((f n)@❨n❩)◗(unwind_gen f q)
+    [ list_empty     ⇒ 𝗱((f n)＠⧣❨n❩)◗(unwind_gen f q)
     | list_lcons _ _ ⇒ unwind_gen f q
     ]
   | label_m   ⇒ unwind_gen f q
@@ -46,7 +46,7 @@ lemma unwind_gen_empty (f):
 // qed.
 
 lemma unwind_gen_d_empty (f) (n):
-      𝗱((f n)@❨n❩)◗𝐞 = ◆[f](𝗱n◗𝐞).
+      𝗱((f n)＠⧣❨n❩)◗𝐞 = ◆[f](𝗱n◗𝐞).
 // qed.
 
 lemma unwind_gen_d_lcons (f) (p) (l) (n):
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
index 9d4955ff9..a9b2683b6 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
@@ -20,7 +20,7 @@ include "ground/relocation/tr_compose_pap.ma".
 (* Properties with tr_compose ***********************************************)
 
 lemma unwind_gen_after (f2) (f1) (p):
-      ◆[f2]◆[f1]p = ◆[λn.(f2 ((f1 n)@❨n❩))∘(f1 n)]p.
+      ◆[f2]◆[f1]p = ◆[λn.(f2 ((f1 n)＠⧣❨n❩))∘(f1 n)]p.
 #f2 #f1 #p @(path_ind_unwind … p) -p //
 #n #_ <unwind_gen_d_empty <unwind_gen_d_empty //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
index 7d75fe605..fcc04282b 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
@@ -74,7 +74,7 @@ qed-.
 (* Advanced constructions with list_rcons ***********************************)
 
 lemma unwind_gen_d_empty_dx (n) (p) (f):
-      (⊗p)◖𝗱((f n)@❨n❩) = ◆[f](p◖𝗱n).
+      (⊗p)◖𝗱((f n)＠⧣❨n❩) = ◆[f](p◖𝗱n).
 #n #p #f <unwind_gen_append_proper_dx // 
 qed.
 
@@ -110,7 +110,7 @@ qed-.
 
 lemma unwind_gen_inv_d_sn (k) (q) (p) (f):
       (𝗱k◗q) = ◆[f]p →
-      ∃∃r,h. 𝐞 = ⊗r & (f h)@❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
+      ∃∃r,h. 𝐞 = ⊗r & (f h)＠⧣❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
 #k #q #p @(path_ind_unwind … p) -p
 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 [ <unwind_gen_empty #H destruct
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma
index e5a6ea13f..3e76deece 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma
@@ -29,8 +29,8 @@ match p with
   match l with
   [ label_d n ⇒
     match q with
-    [ list_empty     ⇒ unwind_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (𝐮❨f@❨n❩❩) q
-    | list_lcons _ _ ⇒ unwind_gen (A) k (𝐮❨f@❨n❩❩) q
+    [ list_empty     ⇒ unwind_gen (A) (λg,p. k g (𝗱(f＠⧣❨n❩)◗p)) (𝐮❨f＠⧣❨n❩❩) q
+    | list_lcons _ _ ⇒ unwind_gen (A) k (𝐮❨f＠⧣❨n❩❩) q
     ]
   | label_m   ⇒ unwind_gen (A) k f q
   | label_L   ⇒ unwind_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q
@@ -64,11 +64,11 @@ lemma unwind_empty (A) (k) (f):
 // qed.
 
 lemma unwind_d_empty (A) (k) (n) (f):
-      ▼❨(λg,p. k g (𝗱(f@❨n❩)◗p)), 𝐮❨f@❨n❩❩, 𝐞❩ = ▼{A}❨k, f, 𝗱n◗𝐞❩.
+      ▼❨(λg,p. k g (𝗱(f＠⧣❨n❩)◗p)), 𝐮❨f＠⧣❨n❩❩, 𝐞❩ = ▼{A}❨k, f, 𝗱n◗𝐞❩.
 // qed.
 
 lemma unwind_d_lcons (A) (k) (p) (l) (n) (f):
-      ▼❨k, 𝐮❨f@❨n❩❩, l◗p❩ = ▼{A}❨k, f, 𝗱n◗l◗p❩.
+      ▼❨k, 𝐮❨f＠⧣❨n❩❩, l◗p❩ = ▼{A}❨k, f, 𝗱n◗l◗p❩.
 // qed.
 
 lemma unwind_m_sn (A) (k) (p) (f):
@@ -94,11 +94,11 @@ lemma unwind_path_empty (f):
 // qed.
 
 lemma unwind_path_d_empty (f) (n):
-      𝗱(f@❨n❩)◗𝐞 = ▼[f](𝗱n◗𝐞).
+      𝗱(f＠⧣❨n❩)◗𝐞 = ▼[f](𝗱n◗𝐞).
 // qed.
 
 lemma unwind_path_d_lcons (f) (p) (l) (n):
-      ▼[𝐮❨f@❨n❩❩](l◗p) = ▼[f](𝗱n◗l◗p).
+      ▼[𝐮❨f＠⧣❨n❩❩](l◗p) = ▼[f](𝗱n◗l◗p).
 // qed.
 
 lemma unwind_path_m_sn (f) (p):
@@ -112,7 +112,7 @@ lemma unwind_rmap_empty (f):
 // qed.
 
 lemma unwind_rmap_d_sn (f) (p) (n):
-      ▼[p](𝐮❨f@❨n❩❩) = ▼[𝗱n◗p]f.
+      ▼[p](𝐮❨f＠⧣❨n❩❩) = ▼[𝗱n◗p]f.
 #f * // qed.
 
 lemma unwind_rmap_m_sn (f) (p):
@@ -145,7 +145,7 @@ qed.
 (* Advanced constructions with proj_rmap and path_rcons *********************)
 
 lemma unwind_rmap_d_dx (f) (p) (n):
-      (𝐮❨(▼[p]f)@❨n❩❩) = ▼[p◖𝗱n]f.
+      (𝐮❨(▼[p]f)＠⧣❨n❩❩) = ▼[p◖𝗱n]f.
 // qed.
 
 lemma unwind_rmap_m_dx (f) (p):
@@ -165,7 +165,7 @@ lemma unwind_rmap_S_dx (f) (p):
 // qed.
 
 lemma unwind_rmap_pap_d_dx (f) (p) (n) (m):
-      ▼[p]f@❨n❩+m = ▼[p◖𝗱n]f@❨m❩.
+      ▼[p]f＠⧣❨n❩+m = ▼[p◖𝗱n]f＠⧣❨m❩.
 #f #p #n #m
 <unwind_rmap_d_dx <tr_uni_pap <pplus_comm //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_constructors.ma
index d2a552d84..a412797a0 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_constructors.ma
@@ -18,20 +18,20 @@ include "delayed_updating/syntax/prototerm_constructors.ma".
 (* UNWIND FOR PROTOTERM *****************************************************)
 
 lemma unwind_iref_sn (f) (t:prototerm) (n:pnat):
-      ▼[𝐮❨f@❨n❩❩]t ⊆ ▼[f](𝛗n.t).
+      ▼[𝐮❨f＠⧣❨n❩❩]t ⊆ ▼[f](𝛗n.t).
 #f #t #n #p * #q #Hq #H0 destruct
 @(ex2_intro … (𝗱n◗𝗺◗q))
 /2 width=1 by in_comp_iref/
 qed-.
 
 lemma unwind_iref_dx (f) (t) (n:pnat):
-      ▼[f](𝛗n.t) ⊆ ▼[𝐮❨f@❨n❩❩]t.
+      ▼[f](𝛗n.t) ⊆ ▼[𝐮❨f＠⧣❨n❩❩]t.
 #f #t #n #p * #q #Hq #H0 destruct
 elim (in_comp_inv_iref … Hq) -Hq #p #Hp #Ht destruct
 /2 width=1 by in_comp_unwind_bi/
 qed-.
 
 lemma unwind_iref (f) (t) (n:pnat):
-      ▼[𝐮❨f@❨n❩❩]t ⇔ ▼[f](𝛗n.t).
+      ▼[𝐮❨f＠⧣❨n❩❩]t ⇔ ▼[f](𝛗n.t).
 /3 width=1 by conj, unwind_iref_sn, unwind_iref_dx/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_depth.ma
index 13d23cbaf..05e2d523b 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_depth.ma
@@ -41,7 +41,7 @@ lemma unwind_rmap_decompose (p) (f):
 qed.
 
 lemma unwind_rmap_pap_le (f) (p) (n):
-      n < ▼❘p❘ → (▼[p]𝐢)@❨n❩ = (▼[p]f)@❨n❩.
+      n < ▼❘p❘ → (▼[p]𝐢)＠⧣❨n❩ = (▼[p]f)＠⧣❨n❩.
 #f #p #n #Hn
 >(tr_pap_eq_repl … (▼[p]f) … (unwind_rmap_decompose …))
 <tr_compose_pap <tr_pap_pushs_le //
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma
index ed025110a..0f52a1858 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma
@@ -74,7 +74,7 @@ qed-.
 (* Advanced constructions with proj_path ************************************)
 
 lemma unwind_path_d_empty_dx (n) (p) (f):
-      (⊗p)◖𝗱((▼[p]f)@❨n❩) = ▼[f](p◖𝗱n).
+      (⊗p)◖𝗱((▼[p]f)＠⧣❨n❩) = ▼[f](p◖𝗱n).
 #n #p #f <unwind_append_proper_dx // 
 qed.
 
@@ -110,7 +110,7 @@ qed-.
 
 lemma unwind_path_inv_d_sn (k) (q) (p) (f):
       (𝗱k◗q) = ▼[f]p →
-      ∃∃r,h. 𝐞 = ⊗r & (▼[r]f)@❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
+      ∃∃r,h. 𝐞 = ⊗r & (▼[r]f)＠⧣❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
 #k #q #p @(path_ind_unwind … p) -p
 [| #n | #n #l #p |*: #p ] [|*: #IH ] #f
 [ <unwind_path_empty #H destruct
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_update.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_update.ma
index 9bdb32cdb..69fcb47d5 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_update.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_update.ma
@@ -23,7 +23,7 @@ include "ground/lib/stream_eq_eq.ma".
 
 lemma unwind_rmap_pap_le (f1) (f2) (p) (m:pnat) (l:nat):
       ninj (m+⧣p+l) = ❘p❘ →
-      (▼[p]f1)@❨m❩ = (▼[p]f2)@❨m❩.
+      (▼[p]f1)＠⧣❨m❩ = (▼[p]f2)＠⧣❨m❩.
 #f1 #f2 #p @(list_ind_rcons … p) -p
 [ #m #l <depth_empty #H0 destruct
 | #p * [ #n ] #IH #m #l
@@ -43,7 +43,7 @@ lemma unwind_rmap_pap_le (f1) (f2) (p) (m:pnat) (l:nat):
 qed.
 
 lemma unwind_rmap_pap_gt (f) (p) (m):
-      f@❨m+⧣p❩+❘p❘ = (▼[p]f)@❨m+❘p❘❩.
+      f＠⧣❨m+⧣p❩+❘p❘ = (▼[p]f)＠⧣❨m+❘p❘❩.
 #f #p @(list_ind_rcons … p) -p [ // ]
 #p * [ #n ] #IH #m
 [ <update_d_dx <depth_d_dx
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma
index 38d063225..2baa23e2f 100644
--- a/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/apply_2.ma
@@ -14,6 +14,6 @@
 
 (* GROUND NOTATION **********************************************************)
 
-notation "hvbox( f @❨ break term 46 a ❩ )"
+notation "hvbox( f ＠❨ break term 46 a ❩ )"
   non associative with precedence 60
   for @{ 'Apply $f $a }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/atsharp_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/atsharp_2.ma
new file mode 100644
index 000000000..697a9a84b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/atsharp_2.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( f ＠⧣❨ break term 46 a ❩ )"
+  non associative with precedence 60
+  for @{ 'AtSharp $f $a }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/rat_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/rat_3.ma
deleted file mode 100644
index 5664826f9..000000000
--- a/matita/matita/contribs/lambdadelta/ground/notation/relations/rat_3.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* GROUND NOTATION **********************************************************)
-
-notation "hvbox( @❨ term 46 T1 , break term 46 f ❩ ≘ break term 46 T2 )"
-  non associative with precedence 45
-  for @{ 'RAt $T1 $f $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/ground/notation/relations/ratsharp_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/relations/ratsharp_3.ma
new file mode 100644
index 000000000..774a29da9
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/notation/relations/ratsharp_3.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* GROUND NOTATION **********************************************************)
+
+notation "hvbox( ＠⧣❨ term 46 T1 , break term 46 f ❩ ≘ break term 46 T2 )"
+  non associative with precedence 45
+  for @{ 'RAtSharp $T1 $f $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma
index 453315c77..0a70d2f45 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/relations/rat_3.ma".
+include "ground/notation/relations/ratsucc_3.ma".
 include "ground/arith/nat_plus.ma".
 include "ground/arith/nat_lt.ma".
 include "ground/relocation/fr2_map.ma".
@@ -34,13 +34,13 @@ inductive fr2_nat: fr2_map → relation nat ≝
 
 interpretation
   "non-negative relational application (finite relocation maps with pairs)"
-  'RAt l1 f l2 = (fr2_nat f l1 l2).
+  'RAtSucc l1 f l2 = (fr2_nat f l1 l2).
 
 (* Basic inversions *********************************************************)
 
 (*** at_inv_nil *)
 lemma fr2_nat_inv_empty (l1) (l2):
-      @❨l1, 𝐞❩ ≘ l2 → l1 = l2.
+      @↑❨l1, 𝐞❩ ≘ l2 → l1 = l2.
 #l1 #l2 @(insert_eq_1 … (𝐞))
 #f * -f -l1 -l2
 [ //
@@ -51,9 +51,9 @@ qed-.
 
 (*** at_inv_cons *)
 lemma fr2_nat_inv_lcons (f) (d) (h) (l1) (l2):
-      @❨l1, ❨d,h❩◗f❩ ≘ l2 →
-      ∨∨ ∧∧ l1 < d & @❨l1, f❩ ≘ l2 
-       | ∧∧ d ≤ l1 & @❨l1+h, f❩ ≘ l2.
+      @↑❨l1, ❨d,h❩◗f❩ ≘ l2 →
+      ∨∨ ∧∧ l1 < d & @↑❨l1, f❩ ≘ l2 
+       | ∧∧ d ≤ l1 & @↑❨l1+h, f❩ ≘ l2.
 #g #d #h #l1 #l2 @(insert_eq_1 … (❨d, h❩◗g))
 #f * -f -l1 -l2
 [ #l #H destruct
@@ -64,7 +64,7 @@ qed-.
 
 (*** at_inv_cons *)
 lemma fr2_nat_inv_lcons_lt (f) (d) (h) (l1) (l2):
-      @❨l1, ❨d,h❩◗f❩ ≘ l2 → l1 < d → @❨l1, f❩ ≘ l2.
+      @↑❨l1, ❨d,h❩◗f❩ ≘ l2 → l1 < d → @↑❨l1, f❩ ≘ l2.
 #f #d #h #l1 #h2 #H
 elim (fr2_nat_inv_lcons … H) -H * // #Hdl1 #_ #Hl1d
 elim (nlt_ge_false … Hl1d Hdl1)
@@ -72,7 +72,7 @@ qed-.
 
 (*** at_inv_cons *)
 lemma fr2_nat_inv_lcons_ge (f) (d) (h) (l1) (l2):
-      @❨l1, ❨d,h❩◗f❩ ≘ l2 → d ≤ l1 → @❨l1+h, f❩ ≘ l2.
+      @↑❨l1, ❨d,h❩◗f❩ ≘ l2 → d ≤ l1 → @↑❨l1+h, f❩ ≘ l2.
 #f #d #h #l1 #h2 #H
 elim (fr2_nat_inv_lcons … H) -H * // #Hl1d #_ #Hdl1
 elim (nlt_ge_false … Hl1d Hdl1)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma
index b4033e80c..c84990142 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma
@@ -20,7 +20,7 @@ include "ground/relocation/fr2_nat.ma".
 
 (*** at_mono *)
 theorem fr2_nat_mono (f) (l):
-        ∀l1. @❨l, f❩ ≘ l1 → ∀l2. @❨l, f❩ ≘ l2 → l1 = l2.
+        ∀l1. @↑❨l, f❩ ≘ l1 → ∀l2. @↑❨l, f❩ ≘ l2 → l1 = l2.
 #f #l #l1 #H elim H -f -l -l1
 [ #l #x #H <(fr2_nat_inv_empty … H) -x //
 | #f #d #h #l #l1 #Hld #_ #IH #x #H
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after_ist.ma
index cb234dc2d..a4e5ecb03 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_after_ist.ma
@@ -28,7 +28,7 @@ definition H_pr_after_inj: predicate pr_map ≝
 
 (*** after_inj_O_aux *)
 corec fact pr_after_inj_unit_aux:
-           ∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_after_inj f1.
+           ∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_after_inj f1.
 #f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
 cases (pr_pat_inv_unit_bi … H1f1) -H1f1 [|*: // ] #g1 #H1
 lapply (pr_ist_inv_push … H2f1 … H1) -H2f1 #H2g1
@@ -45,8 +45,8 @@ qed-.
 
 (*** after_inj_aux *)
 fact pr_after_inj_aux:
-     (∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_after_inj f1) →
-     ∀i2,f1. @❨𝟏, f1❩ ≘ i2 → H_pr_after_inj f1.
+     (∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_after_inj f1) →
+     ∀i2,f1. ＠⧣❨𝟏, f1❩ ≘ i2 → H_pr_after_inj f1.
 #H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
 #i2 #IH #f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
 elim (pr_pat_inv_unit_succ … H1f1) -H1f1 [|*: // ] #g1 #H1g1 #H1
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist.ma
index 9756cd207..62c9f79bd 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_ist.ma
@@ -47,8 +47,8 @@ qed-.
 
 (*** after_at1_fwd *)
 lemma pr_after_des_ist_pat:
-      ∀f1,i1,i2. @❨i1, f1❩ ≘ i2 → ∀f2. 𝐓❨f2❩ → ∀f. f2 ⊚ f1 ≘ f →
-      ∃∃i. @❨i2, f2❩ ≘ i & @❨i1, f❩ ≘ i.
+      ∀f1,i1,i2. ＠⧣❨i1, f1❩ ≘ i2 → ∀f2. 𝐓❨f2❩ → ∀f. f2 ⊚ f1 ≘ f →
+      ∃∃i. ＠⧣❨i2, f2❩ ≘ i & ＠⧣❨i1, f❩ ≘ i.
 #f1 #i1 #i2 #Hf1 #f2 #Hf2 #f #Hf elim (Hf2 i2) -Hf2
 /3 width=8 by pr_after_des_pat, ex2_intro/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat.ma
index c64136a65..41191b21e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat.ma
@@ -21,8 +21,8 @@ include "ground/relocation/pr_after.ma".
 
 (*** after_at_fwd *)
 lemma pr_after_pat_des (i) (i1):
-      ∀f. @❨i1, f❩ ≘ i → ∀f2,f1. f2 ⊚ f1 ≘ f →
-      ∃∃i2. @❨i1, f1❩ ≘ i2 & @❨i2, f2❩ ≘ i.
+      ∀f. ＠⧣❨i1, f❩ ≘ i → ∀f2,f1. f2 ⊚ f1 ≘ f →
+      ∃∃i2. ＠⧣❨i1, f1❩ ≘ i2 & ＠⧣❨i2, f2❩ ≘ i.
 #i elim i -i [2: #i #IH ] #i1 #f #Hf #f2 #f1 #Hf21
 [ elim (pr_pat_inv_succ_dx … Hf) -Hf [1,3:* |*: // ]
   [1: #g #j1 #Hg #H0 #H |2,4: #g #Hg #H ]
@@ -40,8 +40,8 @@ qed-.
 
 (*** after_fwd_at *)
 lemma pr_after_des_pat (i) (i2) (i1):
-      ∀f1,f2. @❨i1, f1❩ ≘ i2 → @❨i2, f2❩ ≘ i →
-      ∀f. f2 ⊚ f1 ≘ f → @❨i1, f❩ ≘ i.
+      ∀f1,f2. ＠⧣❨i1, f1❩ ≘ i2 → ＠⧣❨i2, f2❩ ≘ i →
+      ∀f. f2 ⊚ f1 ≘ f → ＠⧣❨i1, f❩ ≘ i.
 #i elim i -i [2: #i #IH ] #i2 #i1 #f1 #f2 #Hf1 #Hf2 #f #Hf
 [ elim (pr_pat_inv_succ_dx … Hf2) -Hf2 [1,3: * |*: // ]
   #g2 [ #j2 ] #Hg2 [ #H22 ] #H20
@@ -60,16 +60,16 @@ qed-.
 
 (*** after_fwd_at2 *)
 lemma pr_after_des_pat_sn (i1) (i):
-      ∀f. @❨i1, f❩ ≘ i → ∀f1,i2. @❨i1, f1❩ ≘ i2 →
-      ∀f2. f2 ⊚ f1 ≘ f → @❨i2, f2❩ ≘ i.
+      ∀f. ＠⧣❨i1, f❩ ≘ i → ∀f1,i2. ＠⧣❨i1, f1❩ ≘ i2 →
+      ∀f2. f2 ⊚ f1 ≘ f → ＠⧣❨i2, f2❩ ≘ i.
 #i1 #i #f #Hf #f1 #i2 #Hf1 #f2 #H elim (pr_after_pat_des … Hf … H) -f
 #j1 #H #Hf2 <(pr_pat_mono … Hf1 … H) -i1 -i2 //
 qed-.
 
 (*** after_fwd_at1 *)
 lemma pr_after_des_pat_dx (i) (i2) (i1):
-      ∀f,f2. @❨i1, f❩ ≘ i → @❨i2, f2❩ ≘ i →
-      ∀f1. f2 ⊚ f1 ≘ f → @❨i1, f1❩ ≘ i2.
+      ∀f,f2. ＠⧣❨i1, f❩ ≘ i → ＠⧣❨i2, f2❩ ≘ i →
+      ∀f1. f2 ⊚ f1 ≘ f → ＠⧣❨i1, f1❩ ≘ i2.
 #i elim i -i [2: #i #IH ] #i2 #i1 #f #f2 #Hf #Hf2 #f1 #Hf1
 [ elim (pr_pat_inv_succ_dx … Hf) -Hf [1,3: * |*: // ]
   #g [ #j1 ] #Hg [ #H01 ] #H00
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat_tls.ma
index 02f2aee66..67bc5183b 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat_tls.ma
@@ -23,7 +23,7 @@ include "ground/relocation/pr_after.ma".
 (* Note: this requires ↑ on first n *)
 (*** after_tls *)
 lemma pr_after_tls_sn_tls (n):
-      ∀f1,f2,f. @❨𝟏, f1❩ ≘ ↑n →
+      ∀f1,f2,f. ＠⧣❨𝟏, f1❩ ≘ ↑n →
       f1 ⊚ f2 ≘ f → ⫰*[n]f1 ⊚ f2 ≘ ⫰*[n]f.
 #n @(nat_ind_succ … n) -n //
 #n #IH #f1 #f2 #f #Hf1 #Hf
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat_uni_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat_uni_tls.ma
index 588978f6b..335c6b361 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat_uni_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_after_pat_uni_tls.ma
@@ -24,7 +24,7 @@ include "ground/relocation/pr_after_isi.ma".
 
 (*** after_uni_succ_dx *)
 lemma pr_after_pat_uni (i2) (i1):
-      ∀f2. @❨i1, f2❩ ≘ i2 →
+      ∀f2. ＠⧣❨i1, f2❩ ≘ i2 →
       ∀f. f2 ⊚ 𝐮❨i1❩ ≘ f → 𝐮❨i2❩ ⊚ ⫰*[i2] f2 ≘ f.
 #i2 elim i2 -i2
 [ #i1 #f2 #Hf2 #f #Hf
@@ -46,7 +46,7 @@ qed.
 
 (*** after_uni_succ_sn *)
 lemma pr_pat_after_uni_tls (i2) (i1):
-      ∀f2. @❨i1, f2❩ ≘ i2 →
+      ∀f2. ＠⧣❨i1, f2❩ ≘ i2 →
       ∀f. 𝐮❨i2❩ ⊚ ⫰*[i2] f2 ≘ f → f2 ⊚ 𝐮❨i1❩ ≘ f.
 #i2 elim i2 -i2
 [ #i1 #f2 #Hf2 #f #Hf
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma
index e60d548e7..0d0f01e7a 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_coafter_ist.ma
@@ -27,7 +27,7 @@ definition H_pr_coafter_inj: predicate pr_map ≝
 
 (*** coafter_inj_O_aux *)
 corec fact pr_coafter_inj_unit_aux:
-           ∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_inj f1.
+           ∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_inj f1.
 #f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
 cases (pr_pat_inv_unit_bi … H1f1) -H1f1 [ |*: // ] #g1 #H1
 lapply (pr_ist_inv_push … H2f1 … H1) -H2f1 #H2g1
@@ -44,8 +44,8 @@ qed-.
 
 (*** coafter_inj_aux *)
 fact pr_coafter_inj_aux:
-     (∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_inj f1) →
-     ∀i2,f1. @❨𝟏, f1❩ ≘ i2 → H_pr_coafter_inj f1.
+     (∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_inj f1) →
+     ∀i2,f1. ＠⧣❨𝟏, f1❩ ≘ i2 → H_pr_coafter_inj f1.
 #H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
 #i2 #IH #f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
 elim (pr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #H1g1 #H1
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isf.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isf.ma
index 07e81d67a..9c522c5ba 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isf.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isf.ma
@@ -28,7 +28,7 @@ definition H_pr_coafter_des_ist_isf: predicate pr_map ≝
 
 (*** coafter_isfin2_fwd_O_aux *)
 fact pr_coafter_des_ist_isf_unit_aux:
-     ∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_isf f1.
+     ∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_isf f1.
 #f1 #Hf1 #f2 #H
 generalize in match Hf1; generalize in match f1; -f1
 @(pr_isf_ind … H) -f2
@@ -44,8 +44,8 @@ qed-.
 
 (*** coafter_isfin2_fwd_aux *)
 fact pr_coafter_des_ist_isf_aux:
-     (∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_isf f1) →
-     ∀i2,f1. @❨𝟏, f1❩ ≘ i2 → H_pr_coafter_des_ist_isf f1.
+     (∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_isf f1) →
+     ∀i2,f1. ＠⧣❨𝟏, f1❩ ≘ i2 → H_pr_coafter_des_ist_isf f1.
 #H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
 #i2 #IH #f1 #H1f1 #f2 #Hf2 #H2f1 #f #Hf
 elim (pr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isi.ma
index 50a68b5fb..53f51deaf 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_ist_isi.ma
@@ -27,7 +27,7 @@ definition H_pr_coafter_des_ist_sn_isi: predicate pr_map ≝
 
 (*** coafter_fwd_isid2_O_aux *)
 corec fact pr_coafter_des_ist_sn_isi_unit_aux:
-           ∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1.
+           ∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1.
 #f1 #H1f1 #f2 #f #H #H2f1 #Hf
 cases (pr_pat_inv_unit_bi … H1f1) -H1f1 [ |*: // ] #g1 #H1
 lapply (pr_ist_inv_push … H2f1 … H1) -H2f1 #H2g1
@@ -42,8 +42,8 @@ qed-.
 
 (*** coafter_fwd_isid2_aux *)
 fact pr_coafter_des_ist_sn_isi_aux:
-     (∀f1. @❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1) →
-     ∀i2,f1. @❨𝟏, f1❩ ≘ i2 → H_pr_coafter_des_ist_sn_isi f1.
+     (∀f1. ＠⧣❨𝟏, f1❩ ≘ 𝟏 → H_pr_coafter_des_ist_sn_isi f1) →
+     ∀i2,f1. ＠⧣❨𝟏, f1❩ ≘ i2 → H_pr_coafter_des_ist_sn_isi f1.
 #H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
 #i2 #IH #f1 #H1f1 #f2 #f #H #H2f1 #Hf
 elim (pr_pat_inv_unit_succ … H1f1) -H1f1 [ |*: // ] #g1 #Hg1 #H1
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_pat_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_pat_tls.ma
index 935810249..4ebc34b5b 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_pat_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_coafter_pat_tls.ma
@@ -23,7 +23,7 @@ include "ground/relocation/pr_coafter_nat_tls.ma".
 (*** coafter_tls_succ *)
 lemma pr_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 (pr_nat_pred_bi … Hg2) -Hg2 #Hg2
 lapply (pr_coafter_tls_bi_tls … Hg2 … Hg) -Hg #Hg
@@ -35,7 +35,7 @@ qed.
 
 (* Note: parked for now
 lemma coafter_fwd_xpx_pushs:
-      ∀g2,f1,g,i,j. @❨i, g2❩ ≘ j → g2 ~⊚ ⫯*[i]⫯f1 ≘ g →
+      ∀g2,f1,g,i,j. ＠⧣❨i, g2❩ ≘ j → g2 ~⊚ ⫯*[i]⫯f1 ≘ 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
@@ -46,7 +46,7 @@ elim (coafter_inv_ppx … Hf) [|*: // ] -Hf #g #Hg #H destruct
 qed-.
 
 lemma coafter_fwd_xnx_pushs:
-      ∀g2,f1,g,i,j. @❨i, g2❩ ≘ j → g2 ~⊚ ⫯*[i]↑f1 ≘ g →
+      ∀g2,f1,g,i,j. ＠⧣❨i, g2❩ ≘ j → g2 ~⊚ ⫯*[i]↑f1 ≘ 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
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_pat.ma
index 2b09f5c96..b9e277d8e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_isi_pat.ma
@@ -20,20 +20,20 @@ include "ground/relocation/pr_pat_pat_id.ma".
 (* Advanced constructions with pr_isi and pr_pat ****************************)
 
 (*** isid_at *)
-lemma pr_isi_pat (f): (∀i. @❨i,f❩ ≘ i) → 𝐈❨f❩.
+lemma pr_isi_pat (f): (∀i. ＠⧣❨i,f❩ ≘ i) → 𝐈❨f❩.
 /3 width=1 by pr_eq_id_isi, pr_pat_inv_id/
 qed.
 
 (* Inversions with pr_pat ***************************************************)
 
 (*** isid_inv_at *)
-lemma pr_isi_inv_pat (f) (i): 𝐈❨f❩ → @❨i,f❩ ≘ i.
+lemma pr_isi_inv_pat (f) (i): 𝐈❨f❩ → ＠⧣❨i,f❩ ≘ i.
 /3 width=3 by pr_isi_inv_eq_id, pr_pat_id, pr_pat_eq_repl_back/
 qed-.
 
 (* Destructions with pr_pat *************************************************)
 
 (*** isid_inv_at_mono *)
-lemma pr_isi_pat_des (f) (i1) (i2): 𝐈❨f❩ → @❨i1,f❩ ≘ i2 → i1 = i2.
+lemma pr_isi_pat_des (f) (i1) (i2): 𝐈❨f❩ → ＠⧣❨i1,f❩ ≘ i2 → i1 = i2.
 /4 width=3 by pr_isi_inv_eq_id, pr_pat_id_des, pr_pat_eq_repl_fwd/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist.ma
index 2c37fcb86..24628b326 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist.ma
@@ -19,7 +19,7 @@ include "ground/relocation/pr_pat.ma".
 
 (*** istot *)
 definition pr_ist: predicate pr_map ≝
-           λf. ∀i. ∃j. @❨i,f❩ ≘ j.
+           λf. ∀i. ∃j. ＠⧣❨i,f❩ ≘ j.
 
 interpretation
   "totality condition (partial relocation maps)"
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_isi.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_isi.ma
index cfc6baf49..87485963e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_isi.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_isi.ma
@@ -20,7 +20,7 @@ include "ground/relocation/pr_ist.ma".
 (* Advanced constructions with pr_isi ***************************************)
 
 (*** isid_at_total *)
-lemma pr_isi_pat_total: ∀f. 𝐓❨f❩ → (∀i1,i2. @❨i1,f❩ ≘ i2 → i1 = i2) → 𝐈❨f❩.
+lemma pr_isi_pat_total: ∀f. 𝐓❨f❩ → (∀i1,i2. ＠⧣❨i1,f❩ ≘ i2 → i1 = i2) → 𝐈❨f❩.
 #f #H1f #H2f @pr_isi_pat
 #i lapply (H1f i) -H1f *
 #j #Hf >(H2f … Hf) in ⊢ (???%); -H2f //
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
index de3ecfe4e..a65f972bb 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_ist_ist.ma
@@ -23,7 +23,7 @@ include "ground/relocation/pr_ist.ma".
 (* Advanced constructions with pr_pat ***************************************)
 
 (*** at_dec *)
-lemma pr_pat_dec (f) (i1) (i2): 𝐓❨f❩ → Decidable (@❨i1,f❩ ≘ i2).
+lemma pr_pat_dec (f) (i1) (i2): 𝐓❨f❩ → Decidable (＠⧣❨i1,f❩ ≘ i2).
 #f #i1 #i2 #Hf lapply (Hf i1) -Hf *
 #j2 #Hf elim (eq_pnat_dec i2 j2)
 [ #H destruct /2 width=1 by or_introl/
@@ -32,9 +32,9 @@ lemma pr_pat_dec (f) (i1) (i2): 𝐓❨f❩ → Decidable (@❨i1,f❩ ≘ i2).
 qed-.
 
 (*** is_at_dec *)
-lemma is_pr_pat_dec (f) (i2): 𝐓❨f❩ → Decidable (∃i1. @❨i1,f❩ ≘ i2).
+lemma is_pr_pat_dec (f) (i2): 𝐓❨f❩ → Decidable (∃i1. ＠⧣❨i1,f❩ ≘ i2).
 #f #i2 #Hf
-lapply (dec_plt (λi1.@❨i1,f❩ ≘ i2) … (↑i2)) [| * ]
+lapply (dec_plt (λi1.＠⧣❨i1,f❩ ≘ i2) … (↑i2)) [| * ]
 [ /2 width=1 by pr_pat_dec/
 | * /3 width=2 by ex_intro, or_introl/
 | #H @or_intror * #i1 #Hi12
@@ -46,7 +46,7 @@ qed-.
 
 (*** at_ext *)
 corec theorem pr_eq_ext_pat (f1) (f2): 𝐓❨f1❩ → 𝐓❨f2❩ →
-              (∀i,i1,i2. @❨i,f1❩ ≘ i1 → @❨i,f2❩ ≘ i2 → i1 = i2) →
+              (∀i,i1,i2. ＠⧣❨i,f1❩ ≘ i1 → ＠⧣❨i,f2❩ ≘ i2 → i1 = i2) →
               f1 ≐ f2.
 cases (pr_map_split_tl f1) #H1
 cases (pr_map_split_tl f2) #H2
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat.ma
index f61913c80..13154a1bb 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_nat.ma
@@ -19,7 +19,7 @@ include "ground/relocation/pr_pat.ma".
 (* NON-NEGATIVE APPLICATION FOR PARTIAL RELOCATION MAPS *********************)
 
 definition pr_nat: relation3 pr_map nat nat ≝
-           λf,l1,l2. @❨↑l1,f❩ ≘ ↑l2.
+           λf,l1,l2. ＠⧣❨↑l1,f❩ ≘ ↑l2.
 
 interpretation
   "relational non-negative application (partial relocation maps)"
@@ -46,7 +46,7 @@ lemma pr_nat_next (f) (l1) (l2) (g) (k2):
 qed.
 
 lemma pr_nat_pred_bi (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → @↑❨↓i1,f❩ ≘ ↓i2.
+      ＠⧣❨i1,f❩ ≘ i2 → @↑❨↓i1,f❩ ≘ ↓i2.
 #f #i1 #i2
 >(npsucc_pred i1) in ⊢ (%→?); >(npsucc_pred i2) in ⊢ (%→?);
 //
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat.ma
index 104d37c74..0eee75321 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/relations/rat_3.ma".
+include "ground/notation/relations/ratsharp_3.ma".
 include "ground/xoa/ex_3_2.ma".
 include "ground/arith/pnat.ma".
 include "ground/relocation/pr_tl.ma".
@@ -34,19 +34,19 @@ coinductive pr_pat: relation3 pr_map pnat pnat ≝
 
 interpretation
   "relational positive application (partial relocation maps)"
-  'RAt i1 f i2 = (pr_pat f i1 i2).
+  'RAtSharp i1 f i2 = (pr_pat f i1 i2).
 
 (*** H_at_div *)
 definition H_pr_pat_div: relation4 pr_map pr_map pr_map pr_map ≝
            λf2,g2,f1,g1.
-           ∀jf,jg,j. @❨jf,f2❩ ≘ j → @❨jg,g2❩ ≘ j →
-           ∃∃j0. @❨j0,f1❩ ≘ jf & @❨j0,g1❩ ≘ jg.
+           ∀jf,jg,j. ＠⧣❨jf,f2❩ ≘ j → ＠⧣❨jg,g2❩ ≘ j →
+           ∃∃j0. ＠⧣❨j0,f1❩ ≘ jf & ＠⧣❨j0,g1❩ ≘ jg.
 
 (* Basic inversions *********************************************************)
 
 (*** at_inv_ppx *)
 lemma pr_pat_inv_unit_push (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g. 𝟏 = i1 → ⫯g = f → 𝟏 = i2.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g. 𝟏 = i1 → ⫯g = f → 𝟏 = i2.
 #f #i1 #i2 * -f -i1 -i2 //
 [ #f #i1 #i2 #_ #g #j1 #j2 #_ * #_ #x #H destruct
 | #f #i1 #i2 #_ #g #j2 * #_ #x #_ #H elim (eq_inv_pr_push_next … H)
@@ -55,8 +55,8 @@ qed-.
 
 (*** at_inv_npx *)
 lemma pr_pat_inv_succ_push (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f →
-      ∃∃j2. @❨j1,g❩ ≘ j2 & ↑j2 = i2.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f →
+      ∃∃j2. ＠⧣❨j1,g❩ ≘ j2 & ↑j2 = i2.
 #f #i1 #i2 * -f -i1 -i2
 [ #f #g #j1 #j2 #_ * #_ #x #x1 #H destruct
 | #f #i1 #i2 #Hi #g #j1 #j2 * * * #x #x1 #H #Hf >(eq_inv_pr_push_bi … Hf) -g destruct /2 width=3 by ex2_intro/
@@ -66,8 +66,8 @@ qed-.
 
 (*** at_inv_xnx *)
 lemma pr_pat_inv_next (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g. ↑g = f →
-      ∃∃j2. @❨i1,g❩ ≘ j2 & ↑j2 = i2.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g. ↑g = f →
+      ∃∃j2. ＠⧣❨i1,g❩ ≘ j2 & ↑j2 = i2.
 #f #i1 #i2 * -f -i1 -i2
 [ #f #g #j1 #j2 * #_ #_ #x #H elim (eq_inv_pr_next_push … H)
 | #f #i1 #i2 #_ #g #j1 #j2 * #_ #_ #x #H elim (eq_inv_pr_next_push … H)
@@ -79,50 +79,50 @@ qed-.
 
 (*** at_inv_ppn *)
 lemma pr_pat_inv_unit_push_succ (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g,j2. 𝟏 = i1 → ⫯g = f → ↑j2 = i2 → ⊥.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g,j2. 𝟏 = i1 → ⫯g = f → ↑j2 = i2 → ⊥.
 #f #i1 #i2 #Hf #g #j2 #H1 #H <(pr_pat_inv_unit_push … Hf … H1 H) -f -g -i1 -i2
 #H destruct
 qed-.
 
 (*** at_inv_npp *)
 lemma pr_pat_inv_succ_push_unit (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f → 𝟏 = i2 → ⊥.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g,j1. ↑j1 = i1 → ⫯g = f → 𝟏 = i2 → ⊥.
 #f #i1 #i2 #Hf #g #j1 #H1 #H elim (pr_pat_inv_succ_push … Hf … H1 H) -f -i1
 #x2 #Hg * -i2 #H destruct
 qed-.
 
 (*** at_inv_npn *)
 lemma pr_pat_inv_succ_push_succ (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g,j1,j2. ↑j1 = i1 → ⫯g = f → ↑j2 = i2 → @❨j1,g❩ ≘ j2.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g,j1,j2. ↑j1 = i1 → ⫯g = f → ↑j2 = i2 → ＠⧣❨j1,g❩ ≘ j2.
 #f #i1 #i2 #Hf #g #j1 #j2 #H1 #H elim (pr_pat_inv_succ_push … Hf … H1 H) -f -i1
 #x2 #Hg * -i2 #H destruct //
 qed-.
 
 (*** at_inv_xnp *)
 lemma pr_pat_inv_next_unit (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g. ↑g = f → 𝟏 = i2 → ⊥.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g. ↑g = f → 𝟏 = i2 → ⊥.
 #f #i1 #i2 #Hf #g #H elim (pr_pat_inv_next … Hf … H) -f
 #x2 #Hg * -i2 #H destruct
 qed-.
 
 (*** at_inv_xnn *)
 lemma pr_pat_inv_next_succ (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g,j2. ↑g = f → ↑j2 = i2 → @❨i1,g❩ ≘ j2.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g,j2. ↑g = f → ↑j2 = i2 → ＠⧣❨i1,g❩ ≘ j2.
 #f #i1 #i2 #Hf #g #j2 #H elim (pr_pat_inv_next … Hf … H) -f
 #x2 #Hg * -i2 #H destruct //
 qed-.
 
 (*** at_inv_pxp *)
 lemma pr_pat_inv_unit_bi (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → 𝟏 = i1 → 𝟏 = i2 → ∃g. ⫯g = f.
+      ＠⧣❨i1,f❩ ≘ i2 → 𝟏 = i1 → 𝟏 = i2 → ∃g. ⫯g = f.
 #f elim (pr_map_split_tl … f) /2 width=2 by ex_intro/
 #H #i1 #i2 #Hf #H1 #H2 cases (pr_pat_inv_next_unit … Hf … H H2)
 qed-.
 
 (*** at_inv_pxn *)
 lemma pr_pat_inv_unit_succ (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀j2. 𝟏 = i1 → ↑j2 = i2 →
-      ∃∃g. @❨i1,g❩ ≘ j2 & ↑g = f.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀j2. 𝟏 = i1 → ↑j2 = i2 →
+      ∃∃g. ＠⧣❨i1,g❩ ≘ j2 & ↑g = f.
 #f elim (pr_map_split_tl … f)
 #H #i1 #i2 #Hf #j2 #H1 #H2
 [ elim (pr_pat_inv_unit_push_succ … Hf … H1 H H2)
@@ -132,7 +132,7 @@ qed-.
 
 (*** at_inv_nxp *)
 lemma pr_pat_inv_succ_unit (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀j1. ↑j1 = i1 → 𝟏 = i2 → ⊥.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀j1. ↑j1 = i1 → 𝟏 = i2 → ⊥.
 #f elim (pr_map_split_tl f)
 #H #i1 #i2 #Hf #j1 #H1 #H2
 [ elim (pr_pat_inv_succ_push_unit … Hf … H1 H H2)
@@ -142,9 +142,9 @@ qed-.
 
 (*** at_inv_nxn *)
 lemma pr_pat_inv_succ_bi (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀j1,j2. ↑j1 = i1 → ↑j2 = i2 →
-      ∨∨ ∃∃g. @❨j1,g❩ ≘ j2 & ⫯g = f
-       | ∃∃g. @❨i1,g❩ ≘ j2 & ↑g = f.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀j1,j2. ↑j1 = i1 → ↑j2 = i2 →
+      ∨∨ ∃∃g. ＠⧣❨j1,g❩ ≘ j2 & ⫯g = f
+       | ∃∃g. ＠⧣❨i1,g❩ ≘ j2 & ↑g = f.
 #f elim (pr_map_split_tl f) *
 /4 width=7 by pr_pat_inv_next_succ, pr_pat_inv_succ_push_succ, ex2_intro, or_intror, or_introl/
 qed-.
@@ -152,9 +152,9 @@ qed-.
 (* Note: the following inversion lemmas must be checked *)
 (*** at_inv_xpx *)
 lemma pr_pat_inv_push (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g. ⫯g = f →
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g. ⫯g = f →
       ∨∨ ∧∧ 𝟏 = i1 & 𝟏 = i2
-       | ∃∃j1,j2. @❨j1,g❩ ≘ j2 & ↑j1 = i1 & ↑j2 = i2.
+       | ∃∃j1,j2. ＠⧣❨j1,g❩ ≘ j2 & ↑j1 = i1 & ↑j2 = i2.
 #f * [2: #i1 ] #i2 #Hf #g #H
 [ elim (pr_pat_inv_succ_push … Hf … H) -f /3 width=5 by or_intror, ex3_2_intro/
 | >(pr_pat_inv_unit_push … Hf … H) -f /3 width=1 by conj, or_introl/
@@ -163,15 +163,15 @@ qed-.
 
 (*** at_inv_xpp *)
 lemma pr_pat_inv_push_unit (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g. ⫯g = f → 𝟏 = i2 → 𝟏 = i1.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g. ⫯g = f → 𝟏 = i2 → 𝟏 = i1.
 #f #i1 #i2 #Hf #g #H elim (pr_pat_inv_push … Hf … H) -f * //
 #j1 #j2 #_ #_ * -i2 #H destruct
 qed-.
 
 (*** at_inv_xpn *)
 lemma pr_pat_inv_push_succ (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀g,j2. ⫯g = f → ↑j2 = i2 →
-      ∃∃j1. @❨j1,g❩ ≘ j2 & ↑j1 = i1.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀g,j2. ⫯g = f → ↑j2 = i2 →
+      ∃∃j1. ＠⧣❨j1,g❩ ≘ j2 & ↑j1 = i1.
 #f #i1 #i2 #Hf #g #j2 #H elim (pr_pat_inv_push … Hf … H) -f *
 [ #_ * -i2 #H destruct
 | #x1 #x2 #Hg #H1 * -i2 #H destruct /2 width=3 by ex2_intro/
@@ -180,7 +180,7 @@ qed-.
 
 (*** at_inv_xxp *)
 lemma pr_pat_inv_unit_dx (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → 𝟏 = i2 →
+      ＠⧣❨i1,f❩ ≘ i2 → 𝟏 = i2 →
       ∃∃g. 𝟏 = i1 & ⫯g = f.
 #f elim (pr_map_split_tl f)
 #H #i1 #i2 #Hf #H2
@@ -191,9 +191,9 @@ qed-.
 
 (*** at_inv_xxn *)
 lemma pr_pat_inv_succ_dx (f) (i1) (i2):
-      @❨i1,f❩ ≘ i2 → ∀j2.  ↑j2 = i2 →
-      ∨∨ ∃∃g,j1. @❨j1,g❩ ≘ j2 & ↑j1 = i1 & ⫯g = f
-       | ∃∃g. @❨i1,g❩ ≘ j2 & ↑g = f.
+      ＠⧣❨i1,f❩ ≘ i2 → ∀j2.  ↑j2 = i2 →
+      ∨∨ ∃∃g,j1. ＠⧣❨j1,g❩ ≘ j2 & ↑j1 = i1 & ⫯g = f
+       | ∃∃g. ＠⧣❨i1,g❩ ≘ j2 & ↑g = f.
 #f elim (pr_map_split_tl f)
 #H #i1 #i2 #Hf #j2 #H2
 [ elim (pr_pat_inv_push_succ … Hf … H H2) -i2 /3 width=5 by or_introl, ex3_2_intro/
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_basic.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_basic.ma
index ca6abde33..ebe55c37e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_basic.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_basic.ma
@@ -20,14 +20,14 @@ include "ground/relocation/pr_nat_basic.ma".
 
 (*** at_basic_lt *)
 lemma pr_pat_basic_lt (m) (n) (i):
-      ninj i ≤ m → @❨i, 𝐛❨m,n❩❩ ≘ i.
+      ninj i ≤ m → ＠⧣❨i, 𝐛❨m,n❩❩ ≘ i.
 #m #n #i >(npsucc_pred i) #Hmi
 /2 width=1 by pr_nat_basic_lt/
 qed.
 
 (*** at_basic_ge *)
 lemma pr_pat_basic_ge (m) (n) (i):
-      m < ninj i → @❨i, 𝐛❨m,n❩❩ ≘ i+n.
+      m < ninj i → ＠⧣❨i, 𝐛❨m,n❩❩ ≘ i+n.
 #m #n #i >(npsucc_pred i) #Hmi <nrplus_npsucc_sn
 /3 width=1 by pr_nat_basic_ge, nlt_inv_succ_dx/
 qed.
@@ -36,10 +36,10 @@ qed.
 
 (*** at_basic_inv_lt *)
 lemma pr_pat_basic_inv_lt (m) (n) (i) (j):
-      ninj i ≤ m → @❨i, 𝐛❨m,n❩❩ ≘ j → i = j.
+      ninj i ≤ m → ＠⧣❨i, 𝐛❨m,n❩❩ ≘ j → i = j.
 /3 width=4 by pr_pat_basic_lt, pr_pat_mono/ qed-.
 
 (*** at_basic_inv_ge *)
 lemma pr_pat_basic_inv_ge (m) (n) (i) (j):
-      m < ninj i → @❨i, 𝐛❨m,n❩❩ ≘ j → i+n = j.
+      m < ninj i → ＠⧣❨i, 𝐛❨m,n❩❩ ≘ j → i+n = j.
 /3 width=4 by pr_pat_basic_ge, pr_pat_mono/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma
index 29620d121..02af501de 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_eq.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_pat_lt.ma".
 
 (*** at_eq_repl_back *)
 corec lemma pr_pat_eq_repl_back (i1) (i2):
-            pr_eq_repl_back (λf. @❨i1,f❩ ≘ i2).
+            pr_eq_repl_back (λf. ＠⧣❨i1,f❩ ≘ i2).
 #f1 * -f1 -i1 -i2
 [ #f1 #g1 #j1 #j2 #H #H1 #H2 #f2 #H12
   cases (pr_eq_inv_push_sn … H12 … H) -g1 /2 width=2 by pr_pat_refl/
@@ -34,11 +34,11 @@ qed-.
 
 (*** at_eq_repl_fwd *)
 lemma pr_pat_eq_repl_fwd (i1) (i2):
-      pr_eq_repl_fwd (λf. @❨i1,f❩ ≘ i2).
+      pr_eq_repl_fwd (λf. ＠⧣❨i1,f❩ ≘ i2).
 #i1 #i2 @pr_eq_repl_sym /2 width=3 by pr_pat_eq_repl_back/
 qed-.
 
-lemma pr_pat_eq (f): ⫯f ≐ f → ∀i. @❨i,f❩ ≘ i.
+lemma pr_pat_eq (f): ⫯f ≐ f → ∀i. ＠⧣❨i,f❩ ≘ i.
 #f #Hf #i elim i -i
 [ /3 width=3 by pr_pat_eq_repl_back, pr_pat_refl/
 | /3 width=7 by pr_pat_eq_repl_back, pr_pat_push/
@@ -48,7 +48,7 @@ qed.
 (* Inversions with pr_eq ****************************************************)
 
 corec lemma pr_pat_inv_eq (f):
-            (∀i. @❨i,f❩ ≘ i) → ⫯f ≐ f.
+            (∀i. ＠⧣❨i,f❩ ≘ i) → ⫯f ≐ f.
 #Hf
 lapply (Hf (𝟏)) #H
 lapply (pr_pat_des_id … H) -H #H
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_id.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_id.ma
index 013468796..dc29d3c6a 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_id.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_id.ma
@@ -20,13 +20,13 @@ include "ground/relocation/pr_pat_eq.ma".
 (* Constructions with pr_id *************************************************)
 
 (*** id_at *)
-lemma pr_pat_id (i): @❨i,𝐢❩ ≘ i.
+lemma pr_pat_id (i): ＠⧣❨i,𝐢❩ ≘ i.
 /2 width=1 by pr_pat_eq, pr_eq_refl/ qed.
 
 (* Inversions with pr_id ****************************************************)
 
 (*** id_inv_at *)
 lemma pr_pat_inv_id (f):
-      (∀i. @❨i,f❩ ≘ i) → 𝐢 ≐ f.
+      (∀i. ＠⧣❨i,f❩ ≘ i) → 𝐢 ≐ f.
 /3 width=1 by pr_pat_inv_eq, pr_id_eq/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_lt.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_lt.ma
index c58c16172..5fe0250c1 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_lt.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_lt.ma
@@ -22,7 +22,7 @@ include "ground/relocation/pr_pat.ma".
 
 (*** at_increasing *)
 lemma pr_pat_increasing (i2) (i1) (f):
-      @❨i1,f❩ ≘ i2 → i1 ≤ i2.
+      ＠⧣❨i1,f❩ ≘ i2 → i1 ≤ i2.
 #i2 elim i2 -i2
 [ #i1 #f #Hf elim (pr_pat_inv_unit_dx … Hf) -Hf //
 | #i2 #IH * //
@@ -33,14 +33,14 @@ qed-.
 
 (*** at_increasing_strict *)
 lemma pr_pat_increasing_strict (g) (i1) (i2):
-      @❨i1,g❩ ≘ i2 → ∀f. ↑f = g →
-      ∧∧ i1 < i2 & @❨i1,f❩ ≘ ↓i2.
+      ＠⧣❨i1,g❩ ≘ i2 → ∀f. ↑f = g →
+      ∧∧ i1 < i2 & ＠⧣❨i1,f❩ ≘ ↓i2.
 #g #i1 #i2 #Hg #f #H elim (pr_pat_inv_next … Hg … H) -Hg -H
 /4 width=2 by conj, pr_pat_increasing, ple_succ_bi/
 qed-.
 
 (*** at_fwd_id_ex *)
-lemma pr_pat_des_id (f) (i): @❨i,f❩ ≘ i → ⫯⫰f = f.
+lemma pr_pat_des_id (f) (i): ＠⧣❨i,f❩ ≘ i → ⫯⫰f = f.
 #f elim (pr_map_split_tl f) //
 #H #i #Hf elim (pr_pat_inv_next … Hf … H) -Hf -H
 #j2 #Hg #H destruct lapply (pr_pat_increasing … Hg) -Hg
@@ -51,8 +51,8 @@ qed-.
 
 (*** at_le_ex *)
 lemma pr_pat_le_ex (j2) (i2) (f):
-      @❨i2,f❩ ≘ j2 → ∀i1. i1 ≤ i2 →
-      ∃∃j1. @❨i1,f❩ ≘ j1 & j1 ≤ j2.
+      ＠⧣❨i2,f❩ ≘ j2 → ∀i1. i1 ≤ i2 →
+      ∃∃j1. ＠⧣❨i1,f❩ ≘ j1 & j1 ≤ j2.
 #j2 elim j2 -j2 [2: #j2 #IH ] #i2 #f #Hf
 [ elim (pr_pat_inv_succ_dx … Hf) -Hf [1,3: * |*: // ]
   #g [ #x2 ] #Hg [ #H2 ] #H0
@@ -71,7 +71,7 @@ qed-.
 
 (*** at_id_le *)
 lemma pr_pat_id_le (i1) (i2):
-      i1 ≤ i2 → ∀f. @❨i2,f❩ ≘ i2 → @❨i1,f❩ ≘ i1.
+      i1 ≤ i2 → ∀f. ＠⧣❨i2,f❩ ≘ i2 → ＠⧣❨i1,f❩ ≘ i1.
 #i1 #i2 #H
 @(ple_ind_alt … H) -i1 -i2 [ #i2 | #i1 #i2 #_ #IH ] #f #Hf
 lapply (pr_pat_des_id … Hf) #H <H in Hf; -H
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_pat.ma
index 20ce2220b..245583f91 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_pat.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_pat.ma".
 
 (*** at_monotonic *)
 theorem pr_pat_monotonic:
-        ∀j2,i2,f. @❨i2,f❩ ≘ j2 → ∀j1,i1. @❨i1,f❩ ≘ j1 →
+        ∀j2,i2,f. ＠⧣❨i2,f❩ ≘ j2 → ∀j1,i1. ＠⧣❨i1,f❩ ≘ j1 →
         i1 < i2 → j1 < j2.
 #j2 elim j2 -j2
 [ #i2 #f #H2f elim (pr_pat_inv_unit_dx … H2f) -H2f //
@@ -39,7 +39,7 @@ qed-.
 
 (*** at_inv_monotonic *)
 theorem pr_pat_inv_monotonic:
-        ∀j1,i1,f. @❨i1,f❩ ≘ j1 → ∀j2,i2. @❨i2,f❩ ≘ j2 →
+        ∀j1,i1,f. ＠⧣❨i1,f❩ ≘ j1 → ∀j2,i2. ＠⧣❨i2,f❩ ≘ j2 →
         j1 < j2 → i1 < i2.
 #j1 elim j1 -j1
 [ #i1 #f #H1f elim (pr_pat_inv_unit_dx … H1f) -H1f //
@@ -62,7 +62,7 @@ qed-.
 
 (*** at_mono *)
 theorem pr_pat_mono (f) (i):
-        ∀i1. @❨i,f❩ ≘ i1 → ∀i2. @❨i,f❩ ≘ i2 → i2 = i1.
+        ∀i1. ＠⧣❨i,f❩ ≘ i1 → ∀i2. ＠⧣❨i,f❩ ≘ i2 → i2 = i1.
 #f #i #i1 #H1 #i2 #H2 elim (pnat_split_lt_eq_gt i2 i1) //
 #Hi elim (plt_ge_false i i)
 /2 width=6 by pr_pat_inv_monotonic/
@@ -70,7 +70,7 @@ qed-.
 
 (*** at_inj *)
 theorem pr_pat_inj (f) (i):
-        ∀i1. @❨i1,f❩ ≘ i → ∀i2. @❨i2,f❩ ≘ i → i1 = i2.
+        ∀i1. ＠⧣❨i1,f❩ ≘ i → ∀i2. ＠⧣❨i2,f❩ ≘ i → i1 = i2.
 #f #i #i1 #H1 #i2 #H2 elim (pnat_split_lt_eq_gt i2 i1) //
 #Hi elim (plt_ge_false i i)
 /2 width=6 by pr_pat_monotonic/
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_pat_id.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_pat_id.ma
index 90bee366b..be80edf89 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_pat_id.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_pat_id.ma
@@ -21,7 +21,7 @@ include "ground/relocation/pr_pat_pat.ma".
 
 (*** at_id_fwd *)
 lemma pr_pat_id_des (i1) (i2):
-      @❨i1,𝐢❩ ≘ i2 → i1 = i2.
+      ＠⧣❨i1,𝐢❩ ≘ i2 → i1 = i2.
 /2 width=4 by pr_pat_mono/ qed-.
 
 (* Main constructions with pr_id ********************************************)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_tls.ma
index eaaaf0501..1150c6a8d 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_tls.ma
@@ -23,7 +23,7 @@ include "ground/relocation/pr_pat_eq.ma".
 (* Note: this requires ↑ on first n *)
 (*** at_pxx_tls *)
 lemma pr_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 (pr_pat_inv_unit_succ … Hf) -Hf [|*: // ] #g #Hg #H0 destruct
@@ -32,7 +32,7 @@ qed.
 
 (* Note: this requires ↑ on third n2 *)
 (*** at_tls *)
-lemma pr_pat_tls (n2) (f): ⫯⫰*[↑n2]f ≐ ⫰*[n2]f → ∃i1. @❨i1,f❩ ≘ ↑n2.
+lemma pr_pat_tls (n2) (f): ⫯⫰*[↑n2]f ≐ ⫰*[n2]f → ∃i1. ＠⧣❨i1,f❩ ≘ ↑n2.
 #n2 @(nat_ind_succ … n2) -n2
 [ /4 width=4 by pr_pat_eq_repl_back, pr_pat_refl, ex_intro/
 | #n2 #IH #f <pr_tls_swap <pr_tls_swap in ⊢ (??%→?); #H
@@ -47,8 +47,8 @@ qed-.
 (* Note: this does not require ↑ on second and third p *)
 (*** at_inv_nxx *)
 lemma pr_pat_inv_succ_sn (p) (g) (i1) (j2):
-      @❨↑i1,g❩ ≘ j2 → @❨𝟏,g❩ ≘ p →
-      ∃∃i2. @❨i1,⫰*[p]g❩ ≘ i2 & p+i2 = j2.
+      ＠⧣❨↑i1,g❩ ≘ j2 → ＠⧣❨𝟏,g❩ ≘ p →
+      ∃∃i2. ＠⧣❨i1,⫰*[p]g❩ ≘ i2 & p+i2 = j2.
 #p elim p -p
 [ #g #i1 #j2 #Hg #H
   elim (pr_pat_inv_unit_bi … H) -H [|*: // ] #f #H0
@@ -65,7 +65,7 @@ qed-.
 (* Note: this requires ↑ on first n2 *)
 (*** at_inv_tls *)
 lemma pr_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 (pr_pat_inv_unit_dx … Hf) -Hf // #g #H1 #H destruct
   /2 width=1 by pr_eq_refl/
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_uni.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_uni.ma
index 8e9e28a97..f284a8acd 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_uni.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_pat_uni.ma
@@ -22,7 +22,7 @@ include "ground/relocation/pr_pat_pat_id.ma".
 
 (*** at_uni *)
 lemma pr_pat_uni (n) (i):
-      @❨i,𝐮❨n❩❩ ≘ i+n.
+      ＠⧣❨i,𝐮❨n❩❩ ≘ i+n.
 #n @(nat_ind_succ … n) -n
 /2 width=5 by pr_pat_next/
 qed.
@@ -31,5 +31,5 @@ qed.
 
 (*** at_inv_uni *)
 lemma pr_pat_inv_uni (n) (i) (j):
-      @❨i,𝐮❨n❩❩ ≘ j → j = i+n.
+      ＠⧣❨i,𝐮❨n❩❩ ≘ j → j = i+n.
 /2 width=4 by pr_pat_mono/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose.ma
index bbecabe01..a72647d29 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose.ma
@@ -19,7 +19,7 @@ include "ground/relocation/tr_pap.ma".
 
 corec definition tr_compose: tr_map → tr_map → tr_map.
 #f2 * #p1 #f1
-@(stream_cons … (f2@❨p1❩))
+@(stream_cons … (f2＠⧣❨p1❩))
 @(tr_compose ? f1) -tr_compose -f1
 @(⇂*[p1]f2)
 defined.
@@ -32,7 +32,7 @@ interpretation
 
 (*** compose_rew *)
 lemma tr_compose_unfold (f2) (f1):
-      ∀p1. f2@❨p1❩⨮(⇂*[p1]f2)∘f1 = f2∘(p1⨮f1).
+      ∀p1. f2＠⧣❨p1❩⨮(⇂*[p1]f2)∘f1 = f2∘(p1⨮f1).
 #f2 #f1 #p1 <(stream_unfold … (f2∘(p1⨮f1))) //
 qed.
 
@@ -41,7 +41,7 @@ qed.
 (*** compose_inv_rew *)
 lemma tr_compose_inv_unfold (f2) (f1):
       ∀f,p1,p. f2∘(p1⨮f1) = p⨮f →
-      ∧∧ f2@❨p1❩ = p & (⇂*[p1]f2)∘f1 = f.
+      ∧∧ f2＠⧣❨p1❩ = p & (⇂*[p1]f2)∘f1 = f.
 #f2 #f1 #f #p1 #p
 <tr_compose_unfold #H destruct
 /2 width=1 by conj/
@@ -50,7 +50,7 @@ qed-.
 (*** compose_inv_S2 *)
 lemma tr_compose_inv_succ_dx (f2) (f1):
       ∀f,p2,p1,p. (p2⨮f2)∘(↑p1⨮f1) = p⨮f →
-      ∧∧ f2@❨p1❩+p2 = p & f2∘(p1⨮f1) = f2@❨p1❩⨮f.
+      ∧∧ f2＠⧣❨p1❩+p2 = p & f2∘(p1⨮f1) = f2＠⧣❨p1❩⨮f.
 #f2 #f1 #f #p2 #p1 #p
 <tr_compose_unfold #H destruct
 >nsucc_inj <stream_tls_swap
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
index c7f41134f..ba3915a97 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
@@ -44,7 +44,7 @@ include "ground/relocation/tr_pap.ma".
 (*** after_apply *)
 lemma tr_after_pap:
       ∀p1,f2,f1,f. 𝐭❨⇂*[ninj p1]f2❩ ⊚ 𝐭❨f1❩ ≘ 𝐭❨f❩ →
-      (𝐭❨f2❩) ⊚ 𝐭❨p1⨮f1❩ ≘ 𝐭❨f2@❨p1❩⨮f❩.
+      (𝐭❨f2❩) ⊚ 𝐭❨p1⨮f1❩ ≘ 𝐭❨f2＠⧣❨p1❩⨮f❩.
 #p1 elim p1 -p1
 [ * /2 width=1 by tr_after_push_dx/
 | #p1 #IH * #p2 #f2 >nsucc_inj <stream_tls_swap
@@ -113,7 +113,7 @@ lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≐ f.
 
 (* Forward lemmas on after (specific) *****************************************)
 
-lemma after_fwd_hd: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f → f2@❨p1❩ = p.
+lemma after_fwd_hd: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f → f2＠⧣❨p1❩ = p.
 #f2 #f1 #f #p1 #p #H lapply (gr_after_des_pat ? p1 (𝟏) … H) -H [4:|*: // ]
 /3 width=2 by at_inv_O1, sym_eq/
 qed-.
@@ -128,6 +128,6 @@ lemma after_fwd_tls: ∀f,f1,p1,f2,p2,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
 qed-.
 
 lemma after_inv_apply: ∀f2,f1,f,p2,p1,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
-                       (p2⨮f2)@❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f.
+                       (p2⨮f2)＠⧣❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f.
 /3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pap.ma
index 97ffc0d30..7854b2a69 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pap.ma
@@ -21,7 +21,7 @@ include "ground/relocation/tr_pap_tls.ma".
 
 (*** compose_apply *)
 lemma tr_compose_pap (i) (f1) (f2):
-      f2@❨f1@❨i❩❩ = (f2∘f1)@❨i❩.
+      f2＠⧣❨f1＠⧣❨i❩❩ = (f2∘f1)＠⧣❨i❩.
 #i elim i -i
 [ * #p1 #f1 #f2
   <tr_compose_unfold <tr_pap_unit <tr_pap_unit //
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma
index acc891d4b..ec9228378 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_pn.ma
@@ -61,7 +61,7 @@ qed-.
 (*** compose_inv_S1 *)
 lemma tr_compose_inv_next_sn (f2) (f1):
       ∀f,p1,p. (↑f2)∘(p1⨮f1) = p⨮f →
-      ∧∧ ↑(f2@❨p1❩) = p & f2∘(p1⨮f1) = f2@❨p1❩⨮f.
+      ∧∧ ↑(f2＠⧣❨p1❩) = p & f2∘(p1⨮f1) = f2＠⧣❨p1❩⨮f.
 #f2 #f1 #f #p1 #p
 <tr_compose_unfold #H destruct
 /2 width=1 by conj/
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
index 2ff52deec..7d678a7f3 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_tls.ma
@@ -22,7 +22,7 @@ include "ground/arith/nat_rplus_pplus.ma".
 (* Advanced constructions with stream_tls ***********************************)
 
 lemma tr_compose_tls (p) (f1) (f2):
-      (⇂*[f1@❨p❩]f2)∘(⇂*[p]f1) = ⇂*[p](f2∘f1).
+      (⇂*[f1＠⧣❨p❩]f2)∘(⇂*[p]f1) = ⇂*[p](f2∘f1).
 #p elim p -p [| #p #IH ] * #q1 #f1 #f2 //
 <tr_compose_unfold <tr_pap_succ
 >nsucc_inj <stream_tls_succ_lcons <stream_tls_succ_lcons
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
index 9a406ba8c..2deb5bfa0 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
@@ -20,7 +20,7 @@ include "ground/relocation/tr_id_pushs.ma".
 (* Coonstructions with tr_pap ***********************************************)
 
 lemma tr_id_pap (p):
-      p = 𝐢@❨p❩.
+      p = 𝐢＠⧣❨p❩.
 #p >(tr_pushs_id p)
 /2 width=1 by tr_pap_pushs_le/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.ma
index ac2d3fb38..670dbd8ca 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/notation/functions/apply_2.ma".
+include "ground/notation/functions/atsharp_2.ma".
 include "ground/arith/pnat_plus.ma".
 include "ground/relocation/tr_map.ma".
 
@@ -29,16 +29,16 @@ defined.
 
 interpretation
   "functional positive application (total relocation maps)"
-  'Apply f i = (tr_pap i f).
+  'AtSharp f i = (tr_pap i f).
 
 (* Basic constructions ******************************************************)
 
 (*** apply_O1 *)
 lemma tr_pap_unit (f):
-      ∀p. p = (p⨮f)@❨𝟏❩.
+      ∀p. p = (p⨮f)＠⧣❨𝟏❩.
 // qed.
 
 (*** apply_S1 *)
 lemma tr_pap_succ (f):
-      ∀p,i. f@❨i❩+p = (p⨮f)@❨↑i❩.
+      ∀p,i. f＠⧣❨i❩+p = (p⨮f)＠⧣❨↑i❩.
 // qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_eq.ma
index 28a5af264..42d838882 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_eq.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_eq.ma
@@ -21,7 +21,7 @@ include "ground/relocation/tr_pap.ma".
 
 (*** apply_eq_repl *)
 theorem tr_pap_eq_repl (i):
-        stream_eq_repl … (λf1,f2. f1@❨i❩ = f2@❨i❩).
+        stream_eq_repl … (λf1,f2. f1＠⧣❨i❩ = f2＠⧣❨i❩).
 #i elim i -i [2: #i #IH ] * #p1 #f1 * #p2 #f2 #H
 elim (stream_eq_inv_cons_bi … H) -H [1,8: |*: // ] #Hp #Hf //
 <tr_pap_succ <tr_pap_succ /3 width=1 by eq_f2/
@@ -30,7 +30,7 @@ qed.
 (* Main inversions with stream_eq *******************************************)
 
 corec theorem nstream_eq_inv_ext:
-              ∀f1,f2. (∀i. f1@❨i❩ = f2@❨i❩) → f1 ≗ f2.
+              ∀f1,f2. (∀i. f1＠⧣❨i❩ = f2＠⧣❨i❩) → f1 ≗ f2.
 * #p1 #f1 * #p2 #f2 #Hf @stream_eq_cons
 [ @(Hf (𝟏))
 | @nstream_eq_inv_ext -nstream_eq_inv_ext #i
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-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pat.ma
index 90dd95a77..6e5d0c6e6 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pat.ma
@@ -21,7 +21,7 @@ include "ground/relocation/tr_pap.ma".
 (* Constructions with pr_pat ***********************************************)
 
 (*** at_total *)
-lemma tr_pat_total: ∀i1,f. @❨i1,𝐭❨f❩❩ ≘ f@❨i1❩.
+lemma tr_pat_total: ∀i1,f. ＠⧣❨i1,𝐭❨f❩❩ ≘ f＠⧣❨i1❩.
 #i1 elim i1 -i1
 [ * // | #i #IH * /3 width=1 by tr_pat_succ_sn/ ]
 qed.
@@ -30,5 +30,5 @@ qed.
 
 (*** at_inv_total *)
 lemma tr_pat_inv_total (f):
-      ∀i1,i2. @❨i1, 𝐭❨f❩❩ ≘ i2 → f@❨i1❩ = i2.
+      ∀i1,i2. ＠⧣❨i1, 𝐭❨f❩❩ ≘ i2 → f＠⧣❨i1❩ = i2.
 /2 width=6 by pr_pat_mono/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma
index ce4a0aa32..09b342d3d 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma
@@ -20,13 +20,13 @@ include "ground/relocation/tr_pap.ma".
 (* Constructions with tr_push ***********************************************)
 
 lemma tr_pap_push (f):
-      ∀i. ↑(f@❨i❩) = (⫯f)@❨↑i❩.
+      ∀i. ↑(f＠⧣❨i❩) = (⫯f)＠⧣❨↑i❩.
 // qed.
 
 (* Constructions with tr_next ***********************************************)
 
 (*** apply_S2 *)
 lemma tr_pap_next (f):
-      ∀i. ↑(f@❨i❩) = (↑f)@❨i❩.
+      ∀i. ↑(f＠⧣❨i❩) = (↑f)＠⧣❨i❩.
 * #p #f * //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pushs.ma
index 6fe65c8a2..5029eef3e 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pushs.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pushs.ma
@@ -21,7 +21,7 @@ include "ground/relocation/tr_pap_pn.ma".
 (* Constructions with tr_pushs **********************************************)
 
 lemma tr_pap_pushs_le (n) (p) (f):
-      p < ↑n → p = (⫯*[n]f)@❨p❩.
+      p < ↑n → p = (⫯*[n]f)＠⧣❨p❩.
 #n @(nat_ind_succ … n) -n
 [ #p #f #H0
   elim (plt_inv_unit_dx … H0)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
index 678792ff5..da8ea1519 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_tls.ma
@@ -20,7 +20,7 @@ include "ground/lib/stream_tls.ma".
 (* Constructions with stream_tls ********************************************)
 
 lemma tr_pap_plus (p1) (p2) (f):
-      (⇂*[ninj p2]f)@❨p1❩+f@❨p2❩ = f@❨p1+p2❩.
+      (⇂*[ninj p2]f)＠⧣❨p1❩+f＠⧣❨p2❩ = f＠⧣❨p1+p2❩.
 #p1 #p2 elim p2 -p2
 [ * #p #f //
 | #i #IH * #p #f
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pat.ma
index 208d9e7c0..73b6dca66 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pat.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pat.ma
@@ -21,18 +21,18 @@ include "ground/relocation/tr_map.ma".
 (* Constructions with pr_pat ***********************************************)
 
 (*** at_O1 *)
-lemma tr_pat_unit_sn: ∀i2,f. @❨𝟏,𝐭❨i2⨮f❩❩ ≘ i2.
+lemma tr_pat_unit_sn: ∀i2,f. ＠⧣❨𝟏,𝐭❨i2⨮f❩❩ ≘ i2.
 #i2 elim i2 -i2 /2 width=5 by pr_pat_refl, pr_pat_next/
 qed.
 
 (*** at_S1 *)
-lemma tr_pat_succ_sn: ∀p,f,i1,i2. @❨i1, 𝐭❨f❩❩ ≘ i2 → @❨↑i1, 𝐭❨p⨮f❩❩ ≘ i2+p.
+lemma tr_pat_succ_sn: ∀p,f,i1,i2. ＠⧣❨i1, 𝐭❨f❩❩ ≘ i2 → ＠⧣❨↑i1, 𝐭❨p⨮f❩❩ ≘ i2+p.
 #p elim p -p /3 width=7 by pr_pat_push, pr_pat_next/
 qed.
 
 (*** at_plus2 *)
 lemma tr_pat_plus_dx (f):
-      ∀i1,i,p,q. @❨i1, 𝐭❨p⨮f❩❩ ≘ i → @❨i1, 𝐭❨(p+q)⨮f❩❩ ≘ i+q.
+      ∀i1,i,p,q. ＠⧣❨i1, 𝐭❨p⨮f❩❩ ≘ i → ＠⧣❨i1, 𝐭❨(p+q)⨮f❩❩ ≘ i+q.
 #f #i1 #i #p #q #H elim q -q
 /2 width=5 by pr_pat_next/
 qed.
@@ -41,7 +41,7 @@ qed.
 
 (*** at_inv_O1 *)
 lemma tr_pat_inv_unit_sn (f):
-      ∀p,i2. @❨𝟏, 𝐭❨p⨮f❩❩ ≘ i2 → p = i2.
+      ∀p,i2. ＠⧣❨𝟏, 𝐭❨p⨮f❩❩ ≘ i2 → p = i2.
 #f #p elim p -p /2 width=6 by pr_pat_inv_unit_push/
 #p #IH #i2 #H elim (pr_pat_inv_next … H) -H [|*: // ]
 #j2 #Hj * -i2 /3 width=1 by eq_f/
@@ -49,8 +49,8 @@ qed-.
 
 (*** at_inv_S1 *)
 lemma tr_pat_inv_succ_sn (f):
-      ∀p,j1,i2. @❨↑j1, 𝐭❨p⨮f❩❩ ≘ i2 →
-      ∃∃j2. @❨j1, 𝐭❨f❩❩ ≘ j2 & j2+p = i2.
+      ∀p,j1,i2. ＠⧣❨↑j1, 𝐭❨p⨮f❩❩ ≘ i2 →
+      ∃∃j2. ＠⧣❨j1, 𝐭❨f❩❩ ≘ j2 & j2+p = i2.
 #f #p elim p -p /2 width=5 by pr_pat_inv_succ_push/
 #p #IH #j1 #i2 #H elim (pr_pat_inv_next … H) -H [|*: // ]
 #j2 #Hj * -i2 elim (IH … Hj) -IH -Hj
@@ -62,7 +62,7 @@ qed-.
 (* Note: a better conclusion would be: "i1 + ↓p ≤ i2" *)
 (*** at_increasing_plus *)
 lemma tr_pat_increasing_plus (f):
-      ∀p,i1,i2. @❨i1, 𝐭❨p⨮f❩❩ ≘ i2 → i1 + p ≤ ↑i2.
+      ∀p,i1,i2. ＠⧣❨i1, 𝐭❨p⨮f❩❩ ≘ i2 → i1 + p ≤ ↑i2.
 #f #p *
 [ #i2 #H <(tr_pat_inv_unit_sn … H) -i2 //
 | #i1 #i2 #H elim (tr_pat_inv_succ_sn … H) -H
@@ -73,7 +73,7 @@ qed-.
 
 (*** at_fwd_id *)
 lemma tr_pat_des_id (f):
-      ∀p,i. @❨i, 𝐭❨p⨮f❩❩ ≘ i → 𝟏 = p.
+      ∀p,i. ＠⧣❨i, 𝐭❨p⨮f❩❩ ≘ i → 𝟏 = p.
 #f #p #i #H lapply (pr_pat_des_id … H) -H #H
 elim (eq_inv_pr_push_cons … H) -H //
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
index d278582f2..92315b6a6 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
@@ -51,7 +51,7 @@ qed.
 (* Main constructions with tr_compose and tr_tls ****************************)
 
 theorem tr_compose_uni_dx (f) (p):
-        (𝐮❨f@❨p❩❩∘⇂*[p]f) ≗ f∘𝐮❨p❩.
+        (𝐮❨f＠⧣❨p❩❩∘⇂*[p]f) ≗ f∘𝐮❨p❩.
 #f #p
 @nstream_eq_inv_ext #q
 <tr_compose_pap <tr_compose_pap
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_pap.ma
index aa99f8dc3..2a47c4ba8 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_pap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_pap.ma
@@ -21,11 +21,11 @@ include "ground/arith/nat_rplus_succ.ma".
 (* Coonstructions with tr_pap ***********************************************)
 
 lemma tr_uni_pap_unit (n):
-      ↑n = 𝐮❨n❩@❨𝟏❩.
+      ↑n = 𝐮❨n❩＠⧣❨𝟏❩.
 // qed.
 
 lemma tr_uni_pap (n) (p):
-      p + n = 𝐮❨n❩@❨p❩.
+      p + n = 𝐮❨n❩＠⧣❨p❩.
 #n @(nat_ind_succ … n) -n //
 #n #IH * [| #p ] //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 9ee7ad91a..9fed47266 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -22,7 +22,7 @@ table {
   class "green"
   [ { "relocation maps" * } {
       [ { "finite relocation with pairs" * } {
-          [ "fr2_nat ( @❨?,?❩ ≘ ? )" "fr2_nat_nat" * ]
+          [ "fr2_nat ( ＠⧣❨?,?❩ ≘ ? )" "fr2_nat_nat" * ]
           [ "fr2_minus ( ? ▭ ? ≘ ? )" * ]
           [ "fr2_append ( ?●? )" * ]
           [ "fr2_plus ( ?+? )" * ]
@@ -33,7 +33,7 @@ table {
           [ "tr_uni ( 𝐮❨?❩ )" "tr_uni_eq" "tr_uni_hdtl" "tr_uni_tls" "tr_uni_pap" "tr_uni_compose" * ]
           [ "tr_id ( 𝐢 ) " "tr_id_hdtl" "tr_id_pushs" "tr_id_tls" "tr_id_pap" "tr_id_compose" * ]
           [ "tr_compose ( ?∘? )" "tr_compose_eq" "tr_compose_tls" "tr_compose_pn" "tr_compose_pushs" "tr_compose_pap" "tr_compose_compose" * ]
-          [ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_tls" "tr_pap_pat" "tr_pap_pn" "tr_pap_pushs" "tr_pap_pap" * ]
+          [ "tr_pap ( ?＠⧣❨?❩ )" "tr_pap_eq" "tr_pap_tls" "tr_pap_pat" "tr_pap_pn" "tr_pap_pushs" "tr_pap_pap" * ]
           [ "tr_pushs ( ⫯*[?]? )" * ]
           [ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_eq" "tr_pn_hdtl" "tr_pn_tls" * ]
           [ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" "tr_ist" * ]
@@ -53,7 +53,7 @@ table {
           [ "pr_isu ( 𝐔❨?❩ )" "pr_isu_tl" "pr_isu_uni" * ]
           [ "pr_isi ( 𝐈❨?❩ )" "pr_isi_eq" "pr_isi_tl" "pr_isi_pushs" "pr_isi_tls" "pr_isi_id" "pr_isi_uni" "pr_isi_pat" "pr_isi_nat" * ]
           [ "pr_nat ( @↑❨?,?❩ ≘ ? )" "pr_nat_uni" "pr_nat_basic" "pr_nat_nat" * ]
-          [ "pr_pat ( @❨?,?❩ ≘ ? )" "pr_pat_lt" "pr_pat_eq" "pr_pat_tls" "pr_pat_id" "pr_pat_uni" "pr_pat_basic" "pr_pat_pat" "pr_pat_pat_id" * ]
+          [ "pr_pat ( ＠⧣❨?,?❩ ≘ ? )" "pr_pat_lt" "pr_pat_eq" "pr_pat_tls" "pr_pat_id" "pr_pat_uni" "pr_pat_basic" "pr_pat_pat" "pr_pat_pat_id" * ]
           [ "pr_basic ( 𝐛❨?,?❩ )" * ]
           [ "pr_uni ( 𝐮❨?❩ )" "pr_uni_eq" * ]
           [ "pr_id ( 𝐢 ) " "pr_id_eq" * ]
@@ -71,10 +71,10 @@ table {
             "" "" "nstream_isid" "nstream_id ( 𝐢 )" ""
             "" "" "" ""
             "" "" "" "nstream_sor"
-            "" "nstream_istot ( ?@❨?❩ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )"
+            "" "nstream_istot ( ?＠⧣❨?❩ )" "nstream_after ( ? ∘ ? )" "nstream_coafter ( ? ~∘ ? )"
             "nstream_basic" ""
           * ]
-          [ "trace ( ∥?∥ )" "trace_at ( @❨?,?❩ ≘ ? )" "trace_after ( ? ⊚ ? ≘ ? )" "trace_isid ( 𝐈❨?❩ )" "trace_isun ( 𝐔❨?❩ )"
+          [ "trace ( ∥?∥ )" "trace_at ( ＠⧣❨?,?❩ ≘ ? )" "trace_after ( ? ⊚ ? ≘ ? )" "trace_isid ( 𝐈❨?❩ )" "trace_isun ( 𝐔❨?❩ )"
             "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≘ ? )" "trace_snot ( ∁ ? )"
           * ]
         }
diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/drops.ma
index bc55b84ce..cdc06111c 100644
--- a/matita/matita/contribs/lambdadelta/static_2/relocation/drops.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/relocation/drops.ma
@@ -418,12 +418,12 @@ qed-.
 
 (* Properties with application **********************************************)
 
-lemma drops_tls_at: ∀f,i1,i2. @❨i1,f❩ ≘ i2 →
+lemma drops_tls_at: ∀f,i1,i2. ＠⧣❨i1,f❩ ≘ i2 →
                     ∀b,L1,L2. ⇩*[b,⫰*[i2]f] L1 ≘ L2 →
                     ⇩*[b,⫯⫰*[↑i2]f] L1 ≘ L2.
 /3 width=3 by drops_eq_repl_fwd, pr_pat_inv_succ_dx_tls/ qed-.
 
-lemma drops_split_trans_bind2: ∀b,f,I,L,K0. ⇩*[b,f] L ≘ K0.ⓘ[I] → ∀i. @❨O,f❩ ≘ i →
+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.
 #b #f #I #L #K0 #H #i #Hf
 elim (drops_split_trans … H) -H [ |5: @(pr_after_nat_uni … Hf) |2,3: skip ] /2 width=1 by pr_after_isi_dx/ #Y #HLY #H
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 1ec7f4878..88f58f4ea 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1503,6 +1503,7 @@ let load_predefined_virtuals () =
 ;;
 
 let predefined_classes = [
+ ["@"; "ï¼ "; ];
  ["*"; "∗"; ];
  ["/"; "⧸"; ];
  ["&"; "⅋"; ];