From 48b202cd4ccd3ffc10f9a134314f747fdee30d36 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 26 Jan 2012 16:48:05 +0000
Subject: [PATCH] - main lemmas about abstract reducibility candidates closed -
 notation updated (and one bug solved) - Makefile: stats display improved

---
 .../contribs/lambda_delta/Basic_2/Basic_1.txt |  22 +---
 .../lambda_delta/Basic_2/computation/acp.ma   |   4 +-
 .../Basic_2/computation/acp_aaa.ma            |  29 ++---
 .../Basic_2/computation/acp_cr.ma             |  33 ++++--
 .../lambda_delta/Basic_2/computation/lsubc.ma |  66 +++++++++--
 .../Basic_2/computation/lsubc_ldrop.ma        |  68 +++++++++++
 .../Basic_2/computation/lsubc_ldrops.ma       |  32 +++++
 .../lambda_delta/Basic_2/functional/lift.ma   |   4 +-
 .../lambda_delta/Basic_2/functional/rtm.ma    |   4 +-
 .../Basic_2/functional/rtm_step.ma            |  16 +--
 .../lambda_delta/Basic_2/functional/subst.ma  |   8 +-
 .../lambda_delta/Basic_2/grammar/aarity.ma    |  18 ++-
 .../lambda_delta/Basic_2/grammar/cl_shift.ma  |   2 +-
 .../lambda_delta/Basic_2/grammar/cl_weight.ma |   2 +-
 .../lambda_delta/Basic_2/grammar/genv.ma      |  11 +-
 .../lambda_delta/Basic_2/grammar/item.ma      |  16 +--
 .../lambda_delta/Basic_2/grammar/lenv.ma      |  15 ++-
 .../lambda_delta/Basic_2/grammar/lsubs.ma     |  10 +-
 .../lambda_delta/Basic_2/grammar/term.ma      |  37 ++++--
 .../Basic_2/grammar/term_simple.ma            |   8 +-
 .../Basic_2/grammar/term_vector.ma            |   5 +-
 .../lambda_delta/Basic_2/grammar/thom.ma      |  22 ++--
 .../contribs/lambda_delta/Basic_2/names.txt   |  14 +++
 .../contribs/lambda_delta/Basic_2/notation.ma |  66 +++++++----
 .../lambda_delta/Basic_2/reducibility/cpr.ma  |   8 +-
 .../Basic_2/reducibility/cpr_cpr.ma           |   8 +-
 .../Basic_2/reducibility/cpr_lift.ma          |   8 +-
 .../lambda_delta/Basic_2/reducibility/ltpr.ma |  18 +--
 .../lambda_delta/Basic_2/reducibility/tnf.ma  |  28 ++---
 .../lambda_delta/Basic_2/reducibility/tpr.ma  |  94 ++++++++-------
 .../Basic_2/reducibility/tpr_lift.ma          |   8 +-
 .../Basic_2/reducibility/tpr_tpr.ma           |  28 ++---
 .../Basic_2/reducibility/tpr_tpss.ma          |  24 ++--
 .../lambda_delta/Basic_2/reducibility/trf.ma  |  40 +++----
 .../lambda_delta/Basic_2/static/aaa.ma        | 111 ++++++++++++++++--
 .../lambda_delta/Basic_2/static/lsuba.ma      |  16 +--
 .../Basic_2/substitution/gdrop.ma             |   6 +-
 .../Basic_2/substitution/ldrop.ma             |  42 +++----
 .../Basic_2/substitution/ldrop_ldrop.ma       |   4 +-
 .../lambda_delta/Basic_2/substitution/lift.ma |  40 +++----
 .../lambda_delta/Basic_2/substitution/ltps.ma |  42 +++----
 .../Basic_2/substitution/ltps_tps.ma          |   4 +-
 .../lambda_delta/Basic_2/substitution/tps.ma  |  50 ++++----
 .../Basic_2/substitution/tps_lift.ma          |   4 +-
 .../Basic_2/substitution/tps_tps.ma           |  20 ++--
 .../lambda_delta/Basic_2/unfold/delift.ma     |  20 ++--
 .../Basic_2/unfold/delift_lift.ma             |   2 +-
 .../lambda_delta/Basic_2/unfold/ldrops.ma     |   6 +-
 .../lambda_delta/Basic_2/unfold/lifts.ma      |  12 +-
 .../Basic_2/unfold/lifts_vector.ma            |   6 +-
 .../lambda_delta/Basic_2/unfold/ltpss.ma      |  16 +--
 .../Basic_2/unfold/ltpss_ltpss.ma             |   8 +-
 .../lambda_delta/Basic_2/unfold/ltpss_tpss.ma |  16 +--
 .../lambda_delta/Basic_2/unfold/tpss.ma       |  20 ++--
 .../lambda_delta/Basic_2/unfold/tpss_lift.ma  |  12 +-
 .../lambda_delta/Basic_2/unfold/tpss_ltps.ma  |   6 +-
 .../lambda_delta/Ground_2/xoa.conf.xml        |   1 +
 .../contribs/lambda_delta/Ground_2/xoa.ma     |   8 ++
 .../lambda_delta/Ground_2/xoa_notation.ma     |  10 ++
 matita/matita/contribs/lambda_delta/Makefile  |  24 ++--
 60 files changed, 806 insertions(+), 476 deletions(-)
 create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrop.ma
 create mode 100644 matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrops.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt
index 0d06d98b5..67f076030 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt
+++ b/matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt
@@ -74,27 +74,11 @@ csuba/getl csuba_getl_abst
 csuba/getl csuba_getl_abst_rev
 csuba/getl csuba_getl_abbr_rev
 csuba/props csuba_refl
-
-# check #############################################################
-
 csubc/arity csubc_arity_conf
 csubc/arity csubc_arity_trans
-csubc/clear csubc_clear_conf
 csubc/csuba csubc_csuba
 csubc/drop1 drop1_csubc_trans
-csubc/drop1 csubc_drop1_conf_rev
-csubc/drop csubc_drop_conf_O
 csubc/drop drop_csubc_trans
-csubc/drop csubc_drop_conf_rev
-csubc/fwd csubc_gen_sort_l
-csubc/fwd csubc_gen_head_l
-csubc/fwd csubc_gen_sort_r
-csubc/fwd csubc_gen_head_r
-csubc/getl csubc_getl_conf
-csubc/props csubc_refl
-
-# waiting ####################################################################
-
 csubt/clear csubt_clear_conf
 csubt/csuba csubt_csuba
 csubt/drop csubt_drop_flat
@@ -118,10 +102,16 @@ csubv/getl csubv_getl_conf
 csubv/getl csubv_getl_conf_void
 csubv/props csubv_bind_same
 csubv/props csubv_refl
+
+# check #############################################################
+
 drop1/fwd drop1_gen_pnil
 drop1/fwd drop1_gen_pcons
 drop1/props drop1_skip_bind
 drop1/props drop1_cons_tail
+
+# waiting ####################################################################
+
 drop/props drop_ctail
 ex0/props aplus_gz_le
 ex0/props aplus_gz_ge
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma
index 3e13d9ac3..ca1ba4686 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp.ma
@@ -20,10 +20,10 @@ definition CP1 ≝ λRR:lenv→relation term. λRS:relation term.
                  ∀L,k. NF … (RR L) RS (⋆k).
 
 definition CP2 ≝ λRR:lenv→relation term. λRS:relation term.
-                 ∀L,K,W,i. ⇩[0,i] L ≡ K. 𝕓{Abst} W → NF … (RR L) RS (#i).
+                 ∀L,K,W,i. ⇩[0,i] L ≡ K. ⓛW → NF … (RR L) RS (#i).
 
 definition CP3 ≝ λRR:lenv→relation term. λRP:lenv→predicate term.
-                 ∀L,V,k. RP L (𝕔{Appl}⋆k.V) → RP L V.
+                 ∀L,V,k. RP L (ⓐ⋆k.V) → RP L V.
 
 definition CP4 ≝ λRR:lenv→relation term. λRS:relation term.
                  ∀L0,L,T,T0,d,e. NF … (RR L) RS T → 
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma
index 96efde77b..0f70ef703 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_aaa.ma
@@ -12,22 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic_2/unfold/gr2_gr2.ma".
 include "Basic_2/unfold/lifts_lifts.ma".
 include "Basic_2/unfold/ldrops_ldrops.ma".
-include "Basic_2/computation/lsubc.ma".
-
-(* NOTE: The constant (0) can not be generalized *)
-axiom lsubc_ldrop_trans: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
-                         ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 [RP] ⊑ K2.
-
-axiom ldrops_lsubc_trans: ∀RP,L1,K1,des. ⇩*[des] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 →
-                          ∃∃L2. L1 [RP] ⊑ L2 & ⇩*[des] L2 ≡ K2.
-
-axiom aaa_mono: ∀L,T,A1. L ⊢ T ÷ A1 → ∀A2. L ⊢ T ÷ A2 → A1 = A2.
-
-axiom aaa_lifts: ∀L1,L2,T1,T2,A,des.
-                 L1 ⊢ T1 ÷ A → ⇩*[des] L2 ≡ L1 → ⇧*[des] T1 ≡ T2 → L2 ⊢ T2 ÷ A.
+include "Basic_2/static/aaa_lifts.ma".
+include "Basic_2/static/aaa_aaa.ma".
+include "Basic_2/computation/lsubc_ldrops.ma".
 
 (* ABSTRACT COMPUTATION PROPERTIES ******************************************)
 
@@ -41,7 +30,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
 #RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A
 [ #L #k #L0 #des #HL0 #X #H #L2 #HL20
   >(lifts_inv_sort1 … H) -H
-  lapply (aacr_acr … H1RP H2RP 𝕒) #HAtom
+  lapply (aacr_acr … H1RP H2RP ⓪) #HAtom
   @(s2 … HAtom … ◊) // /2 width=2/
 | #I #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20
   lapply (aacr_acr … H1RP H2RP B) #HB
@@ -50,7 +39,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
   elim (ldrops_ldrop_trans … HL01 … HLK1) #X #des1 #i0 #HL0 #H #Hi0 #Hdes1
   >(at_mono … Hi1 … Hi0) -i1
   elim (ldrops_inv_skip2 … Hdes1 … H) -des1 #K0 #V0 #des0 #Hdes0 #HK01 #HV10 #H destruct
-  elim (lsubc_ldrop_trans … HL20 … HL0) -HL0 #X #HLK2 #H
+  elim (lsubc_ldrop_O1_trans … HL20 … HL0) -HL0 #X #HLK2 #H
   elim (lsubc_inv_pair2 … H) -H *
   [ #K2 #HK20 #H destruct
     generalize in match HLK2; generalize in match I; -HLK2 -I * #HLK2
@@ -62,7 +51,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
   | -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0
     #K2 #V2 #A2 #HKV2A #HKV0A #_ #H1 #H2 destruct
     lapply (ldrop_fwd_ldrop2 … HLK2) #HLK2b
-    lapply (aaa_lifts … HKV1B HK01 HV10) -HKV1B -HK01 -HV10 #HKV0B
+    lapply (aaa_lifts … HK01 … HV10 HKV1B) -HKV1B -HK01 -HV10 #HKV0B
     >(aaa_mono … HKV0A … HKV0B) in HKV2A; -HKV0A -HKV0B #HKV2B
     elim (lift_total V2 0 (i0 +1)) #V #HV2
     @(s4 … HB … ◊ … HV2 HLK2)
@@ -82,9 +71,9 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
   | -IHB
     #L3 #V3 #T3 #des3 #HL32 #HT03 #HB
     elim (lifts_total des3 W0) #W2 #HW02
-    elim (ldrops_lsubc_trans … HL32 … HL02) -L2 #L2 #HL32 #HL20
-    lapply (aaa_lifts ? L2 ? W2 ? (des @ des3) HLWB ? ?) -HLWB /2 width=3/ #HLW2B
-    @(IHA (L2. 𝕓{Abst} W2) … (des + 1 @ des3 + 1)) -IHA
+    elim (ldrops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
+    lapply (aaa_lifts … L2 W2 … (des @ des3) … HLWB) -HLWB /2 width=3/ #HLW2B
+    @(IHA (L2. ⓛW2) … (des + 1 @ des3 + 1)) -IHA
     /2 width=3/ /3 width=5/
   ]
 | #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma
index 9908cfd16..9f94d8969 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/acp_cr.ma
@@ -13,7 +13,9 @@
 (**************************************************************************)
 
 include "Basic_2/grammar/aarity.ma".
+include "Basic_2/unfold/gr2_gr2.ma".
 include "Basic_2/unfold/lifts_lift_vector.ma".
+include "Basic_2/unfold/ldrops_ldrop.ma".
 include "Basic_2/computation/acp.ma".
 
 (* ABSTRACT COMPUTATION PROPERTIES ******************************************)
@@ -29,18 +31,18 @@ definition S2 ≝ λRR:lenv→relation term. λRS:relation term. λRP,C:lenv→p
 
 (* Note: this is Tait's ii *)
 definition S3 ≝ λRP,C:lenv→predicate term.
-                ∀L,Vs,V,T,W. C L (ⒶVs. 𝕔{Abbr}V. T) → RP L W → C L (ⒶVs. 𝕔{Appl}V. 𝕔{Abst}W. T).
+                ∀L,Vs,V,T,W. C L (ⒶVs. ⓓV. T) → RP L W → C L (ⒶVs. ⓐV. ⓛW. T).
 
 definition S4 ≝ λRP,C:lenv→predicate term. ∀L,K,Vs,V1,V2,i.
                 C L (ⒶVs. V2) → ⇧[0, i + 1] V1 ≡ V2 →
-                ⇩[0, i] L ≡ K. 𝕓{Abbr} V1 → C L (Ⓐ Vs. #i).
+                ⇩[0, i] L ≡ K. ⓓV1 → C L (Ⓐ Vs. #i).
 
 definition S5 ≝ λRP,C:lenv→predicate term.
                 ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
-                ∀V,T. C (L. 𝕓{Abbr}V) (ⒶV2s. T) → RP L V → C L (ⒶV1s. 𝕔{Abbr}V. T).
+                ∀V,T. C (L. ⓓV) (ⒶV2s. T) → RP L V → C L (ⒶV1s. ⓓV. T).
 
 definition S6 ≝ λRP,C:lenv→predicate term.
-                ∀L,Vs,T,W. C L (ⒶVs. T) → RP L W → C L (ⒶVs. 𝕔{Cast}W. T).
+                ∀L,Vs,T,W. C L (ⒶVs. T) → RP L W → C L (ⒶVs. ⓣW. T).
 
 definition S7 ≝ λC:lenv→predicate term. ∀L1,L2,T1,T2,d,e.
                 C L1 T1 → ⇩[d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C L2 T2.
@@ -65,7 +67,7 @@ let rec aacr (RP:lenv→predicate term) (A:aarity) (L:lenv) on A: predicate term
 λT. match A with
 [ AAtom     ⇒ RP L T
 | APair B A ⇒ ∀L0,V0,T0,des. aacr RP B L0 V0 → ⇩*[des] L0 ≡ L → ⇧*[des] T ≡ T0 →
-              aacr RP A L0 (𝕔{Appl} V0. T0)
+              aacr RP A L0 (ⓐV0. T0)
 ].
 
 interpretation
@@ -99,9 +101,8 @@ lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) →
 @conj /2 width=1/ /2 width=6 by rp_lifts/
 qed.
 
-axiom aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
                 ∀A. acr RR RS RP (aacr RP A).
-(*
 #RR #RS #RP #H1RP #H2RP #A elim A -A normalize //
 #B #A #IHB #IHA @mk_acr normalize
 [ #L #T #H
@@ -119,6 +120,16 @@ axiom aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
   elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct
   elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
   @(s3 … IHA … (V0 :: V0s)) /2 width=6 by rp_lifts/ /4 width=5/
+| #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HB #HL0 #H
+  elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
+  elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct
+  elim (ldrops_ldrop_trans … HL0 … HLK) #X #des0 #i1 #HL02 #H #Hi1 #Hdes0
+  >(at_mono … Hi1 … Hi0) in HL02; -i1 #HL02
+  elim (ldrops_inv_skip2 … Hdes0 … H) -H -des0 #L2 #W1 #des0 #Hdes0 #HLK #HVW1 #H destruct
+  elim (lift_total W1 0 (i0 + 1)) #W2 #HW12
+  elim (lifts_lift_trans … HVW1 … HW12 … Hdes0) // -Hdes0 -Hi0 #V3 #HV13 #HVW2
+  >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2
+  @(s4 … IHA … (V0 :: V0s) … HW12 HL02) /3 width=4/
 | #L #V1s #V2s #HV12s #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H
   elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct
   elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct
@@ -127,7 +138,7 @@ axiom aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
   @(s5 … IHA … (V10 :: V10s) (V20 :: V20s)) /2 width=1/ /2 width=6 by rp_lifts/
   @(HA … (des + 1)) /2 width=1/
   [ @(s7 … IHB … HB … HV120) /2 width=1/
-  | @liftsv_applv //
+  | @lifts_applv //
     elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s
     >(liftv_mono … HV12s … HV10s) -V1s //
   ]
@@ -138,13 +149,13 @@ axiom aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
 | /3 width=7/
 ]
 qed.
-*)
+
 lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
                  ∀L,W,T,A,B. RP L W → (
                     ∀L0,V0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[des + 1] T ≡ T0 →
-                                   ⦃L0, V0⦄ [RP] ϵ 〚B〛 → ⦃L0. 𝕓{Abbr} V0, T0⦄ [RP] ϵ 〚A〛
+                                   ⦃L0, V0⦄ [RP] ϵ 〚B〛 → ⦃L0. ⓓV0, T0⦄ [RP] ϵ 〚A〛
                  ) →
-                 ⦃L, 𝕓{Abst} W. T⦄ [RP] ϵ 〚𝕔 B. A〛.
+                 ⦃L, ⓛW. T⦄ [RP] ϵ 〚②B. A〛.
 #RR #RS #RP #H1RP #H2RP #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HB #HL0 #H
 lapply (aacr_acr … H1RP H2RP A) #HCA
 lapply (aacr_acr … H1RP H2RP B) #HCB
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma
index 695213214..e61c2081d 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc.ma
@@ -19,9 +19,9 @@ include "Basic_2/computation/acp_cr.ma".
 
 inductive lsubc (RP:lenv→predicate term): relation lenv ≝
 | lsubc_atom: lsubc RP (⋆) (⋆)
-| lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1. 𝕓{I} V) (L2. 𝕓{I} V)
+| lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1. ⓑ{I} V) (L2. ⓑ{I} V)
 | lsubc_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ [RP] ϵ 〚A〛 → L2 ⊢ W ÷ A →
-              lsubc RP L1 L2 → lsubc RP (L1. 𝕓{Abbr} V) (L2. 𝕓{Abst} W)
+              lsubc RP L1 L2 → lsubc RP (L1. ⓓV) (L2. ⓛW)
 .
 
 interpretation
@@ -30,27 +30,75 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀I,K2,W. L2 = K2. 𝕓{I} W →
-                          (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. 𝕓{I} W) ∨
+fact lsubc_inv_atom1_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → L1 = ⋆ → L2 = ⋆.
+#RP #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #A #_ #_ #_ #H destruct
+]
+qed.
+
+(* Basic_1: was: csubc_gen_sort_r *)
+lemma lsubc_inv_atom1: ∀RP,L2. ⋆ [RP] ⊑ L2 → L2 = ⋆.
+/2 width=4/ qed-.
+
+fact lsubc_inv_pair1_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀I,K1,V. L1 = K1. ⓑ{I} V →
+                          (∃∃K2. K1 [RP] ⊑ K2 & L2 = K2. ⓑ{I} V) ∨
+                          ∃∃K2,W,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ÷ A &
+                                    K1 [RP] ⊑ K2 &
+                                    L2 = K2. ⓛW & I = Abbr.
+#RP #L1 #L2 * -L1 -L2
+[ #I #K1 #V #H destruct
+| #J #L1 #L2 #V #HL12 #I #K1 #W #H destruct /3 width=3/
+| #L1 #L2 #V1 #W2 #A #HV1 #HW2 #HL12 #I #K1 #V #H destruct /3 width=7/
+]
+qed.
+
+(* Basic_1: was: csubc_gen_head_r *)
+lemma lsubc_inv_pair1: ∀RP,I,K1,L2,V. K1. ⓑ{I} V [RP] ⊑ L2 →
+                       (∃∃K2. K1 [RP] ⊑ K2 & L2 = K2. ⓑ{I} V) ∨
+                       ∃∃K2,W,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ÷ A &
+                                 K1 [RP] ⊑ K2 &
+                                 L2 = K2. ⓛW & I = Abbr.
+/2 width=3/ qed-.
+
+fact lsubc_inv_atom2_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → L2 = ⋆ → L1 = ⋆.
+#RP #L1 #L2 * -L1 -L2
+[ //
+| #I #L1 #L2 #V #_ #H destruct
+| #L1 #L2 #V #W #A #_ #_ #_ #H destruct
+]
+qed.
+
+(* Basic_1: was: csubc_gen_sort_l *)
+lemma lsubc_inv_atom2: ∀RP,L1. L1 [RP] ⊑ ⋆ → L1 = ⋆.
+/2 width=4/ qed-.
+
+fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W →
+                          (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. ⓑ{I} W) ∨
                           ∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ÷ A &
                                     K1 [RP] ⊑ K2 &
-                                    L1 = K1. 𝕓{Abbr} V & I = Abst.
+                                    L1 = K1. ⓓV & I = Abst.
 #RP #L1 #L2 * -L1 -L2
 [ #I #K2 #W #H destruct
 | #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
-| #L1 #L2 #V1 #W2 #A #H #HV1 #HW2 #I #K2 #W #H destruct /3 width=7/
+| #L1 #L2 #V1 #W2 #A #HV1 #HW2 #HL12 #I #K2 #W #H destruct /3 width=7/
 ]
 qed.
 
-lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 [RP] ⊑ K2. 𝕓{I} W →
-                       (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. 𝕓{I} W) ∨
+(* Basic_1: was: csubc_gen_head_l *)
+lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 [RP] ⊑ K2. ⓑ{I} W →
+                       (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. ⓑ{I} W) ∨
                        ∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ÷ A &
                                  K1 [RP] ⊑ K2 &
-                                 L1 = K1. 𝕓{Abbr} V & I = Abst.
+                                 L1 = K1. ⓓV & I = Abst.
 /2 width=3/ qed-.
 
 (* Basic properties *********************************************************)
 
+(* Basic_1: was: csubc_refl *)
 lemma lsubc_refl: ∀RP,L. L [RP] ⊑ L.
 #RP #L elim L -L // /2 width=1/
 qed.
+
+(* Basic_1: removed theorems 2: csubc_clear_conf csubc_getl_conf *)
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrop.ma
new file mode 100644
index 000000000..fcc7f683d
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrop.ma
@@ -0,0 +1,68 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "Basic_2/static/aaa_lift.ma".
+include "Basic_2/computation/acp_cr.ma".
+include "Basic_2/computation/lsubc.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
+
+(* Properties concerning basic local environment slicing ********************)
+
+(* Basic_1: was: csubc_drop_conf_O *)
+(* Note: the constant (0) can not be generalized *)
+lemma lsubc_ldrop_O1_trans: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀K2,e. ⇩[0, e] L2 ≡ K2 →
+                            ∃∃K1. ⇩[0, e] L1 ≡ K1 & K1 [RP] ⊑ K2.
+#RP #L1 #L2 #H elim H -L1 -L2
+[ #X #e #H
+  >(ldrop_inv_atom1 … H) -H /2 width=3/
+| #I #L1 #L2 #V #_ #IHL12 #X #e #H
+  elim (ldrop_inv_O1 … H) -H * #He #H destruct
+  [ elim (IHL12 L2 0 ?) -IHL12 // #X #H <(ldrop_inv_refl … H) -H /3 width=3/
+  | elim (IHL12 … H) -L2 /3 width=3/
+  ]
+| #L1 #L2 #V #W #A #HV #HW #_ #IHL12 #X #e #H
+  elim (ldrop_inv_O1 … H) -H * #He #H destruct
+  [ elim (IHL12 L2 0 ?) -IHL12 // #X #H <(ldrop_inv_refl … H) -H /3 width=7/
+  | elim (IHL12 … H) -L2 /3 width=3/
+  ]
+qed-.
+
+(* Basic_1: was: csubc_drop_conf_rev *)
+lemma ldrop_lsubc_trans: ∀RR,RS,RP.
+                         acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+                         ∀L1,K1,d,e. ⇩[d, e] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 →
+                         ∃∃L2. L1 [RP] ⊑ L2 & ⇩[d, e] L2 ≡ K2.
+#RR #RS #RP #Hacp #Hacr #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+[ #d #e #X #H
+  >(lsubc_inv_atom1 … H) -H /2 width=3/
+| #L1 #I #V1 #X #H
+  elim (lsubc_inv_pair1 … H) -H *
+  [ #K1 #HLK1 #H destruct /3 width=3/
+  | #K1 #W1 #A #HV1 #HW1 #HLK1 #H1 #H2 destruct /3 width=3/
+  ]
+| #L1 #K1 #I #V1 #e #_ #IHLK1 #K2 #HK12
+  elim (IHLK1 … HK12) -K1 /3 width=5/
+| #L1 #K1 #I #V1 #V2 #d #e #HLK1 #HV21 #IHLK1 #X #H
+  elim (lsubc_inv_pair1 … H) -H *
+  [ #K2 #HK12 #H destruct
+    elim (IHLK1 … HK12) -K1 /3 width=5/
+  | #K2 #W2 #A #HV2 #HW2 #HK12 #H1 #H2 destruct
+    elim (IHLK1 … HK12) #K #HL1K #HK2
+    lapply (aacr_acr … Hacp Hacr A) -Hacp -Hacr #HA
+    lapply (s7 … HA … HV2 HLK1 HV21) -HV2
+    elim (lift_total W2 d e) /4 width=9/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrops.ma b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrops.ma
new file mode 100644
index 000000000..95879a234
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/Basic_2/computation/lsubc_ldrops.ma
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "Basic_2/computation/lsubc_ldrop.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
+
+(* Properties concerning generic local environment slicing ******************)
+
+(* Basic_1: was: csubc_drop1_conf_rev *)
+lemma ldrops_lsubc_trans: ∀RR,RS,RP.
+                          acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+                          ∀L1,K1,des. ⇩*[des] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 →
+                          ∃∃L2. L1 [RP] ⊑ L2 & ⇩*[des] L2 ≡ K2.
+#RR #RS #RP #Hacp #Hacr #L1 #K1 #des #H elim H -L1 -K1 -des
+[ /2 width=3/
+| #L1 #L #K1 #des #d #e #_ #HLK1 #IHL #K2 #HK12
+  elim (ldrop_lsubc_trans … Hacp Hacr … HLK1 … HK12) -Hacp -Hacr -K1 #K #HLK #HK2
+  elim (IHL … HLK) -IHL -HLK /3 width=5/
+]
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/functional/lift.ma
index 90e41e9a5..780467209 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/functional/lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/functional/lift.ma
@@ -24,8 +24,8 @@ let rec flift d e U on U ≝ match U with
   | GRef _ ⇒ U
   ]
 | TPair I V T ⇒ match I with
-  [ Bind I ⇒ 𝕓{I} (flift d e V). (flift (d+1) e T)
-  | Flat I ⇒ 𝕗{I} (flift d e V). (flift d e T)
+  [ Bind2 I ⇒ ⓑ{I} (flift d e V). (flift (d+1) e T)
+  | Flat2 I ⇒ ⓕ{I} (flift d e V). (flift d e T)
   ]
 ].
 
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm.ma b/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm.ma
index b15db8653..845e8a04d 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm.ma
@@ -26,8 +26,8 @@ inductive xenv: Type[0] ≝
 interpretation "atom (ext. local environment)"
    'Star = XAtom.
 
-interpretation "environment binding construction (quad)"
-   'DBind L I u K V = (XQuad L I u K V).
+interpretation "environment construction (quad)"
+   'DxItem4 L I u K V = (XQuad L I u K V).
 
 (* machine stack *)
 definition stack: Type[0] ≝ list2 xenv term.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm_step.ma b/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm_step.ma
index e1fabb8fa..c1dc7dcb1 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm_step.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/functional/rtm_step.ma
@@ -28,28 +28,28 @@ inductive rtm_step: relation rtm ≝
               rtm_step (mk_rtm G u (E. ④{Abst} {t, F, V}) S (#0))
                        (mk_rtm G u F S V)
 | rtm_gdrop : ∀G,I,V,u,E,S,p. p < |G| →
-              rtm_step (mk_rtm (G. 𝕓{I} V) u E S (§p))
+              rtm_step (mk_rtm (G. ⓑ{I} V) u E S (§p))
                        (mk_rtm G u E S (§p))
 | rtm_gdelta: ∀G,V,u,E,S,p. p = |G| →
-              rtm_step (mk_rtm (G. 𝕓{Abbr} V) u E S (§p))
+              rtm_step (mk_rtm (G. ⓓV) u E S (§p))
                        (mk_rtm G u E S V)
 | rtm_gtype : ∀G,V,u,E,S,p. p = |G| →
-              rtm_step (mk_rtm (G. 𝕓{Abst} V) u E S (§p))
+              rtm_step (mk_rtm (G. ⓛV) u E S (§p))
                        (mk_rtm G u E S V)
 | rtm_tau   : ∀G,u,E,S,W,T.
-              rtm_step (mk_rtm G u E S (𝕔{Cast} W. T))
+              rtm_step (mk_rtm G u E S (ⓣW. T))
                        (mk_rtm G u E S T)
 | rtm_appl  : ∀G,u,E,S,V,T.
-              rtm_step (mk_rtm G u E S (𝕔{Appl} V. T))
+              rtm_step (mk_rtm G u E S (ⓐV. T))
                        (mk_rtm G u E ({E, V} :: S) T)
 | rtm_beta  : ∀G,u,E,F,V,S,W,T.
-              rtm_step (mk_rtm G u E ({F, V} :: S) (𝕔{Abst} W. T))
+              rtm_step (mk_rtm G u E ({F, V} :: S) (ⓛW. T))
                        (mk_rtm G u (E. ④{Abbr} {u, F, V}) S T)
 | rtm_push  : ∀G,u,E,W,T.
-              rtm_step (mk_rtm G u E ⟠ (𝕔{Abst} W. T))
+              rtm_step (mk_rtm G u E ⟠ (ⓛW. T))
                        (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) ⟠ T)
 | rtm_theta : ∀G,u,E,S,V,T.
-              rtm_step (mk_rtm G u E S (𝕔{Abbr} V. T))
+              rtm_step (mk_rtm G u E S (ⓓV. T))
                        (mk_rtm G u (E. ④{Abbr} {u, E, V}) S T)
 .
 
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma b/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma
index d415c19d6..b12e9b413 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/functional/subst.ma
@@ -24,8 +24,8 @@ let rec fsubst W d U on U ≝ match U with
   | GRef _ ⇒ U
   ]
 | TPair I V T ⇒ match I with
-  [ Bind I ⇒ 𝕓{I} (fsubst W d V). (fsubst W (d+1) T)
-  | Flat I ⇒ 𝕗{I} (fsubst W d V). (fsubst W d T)
+  [ Bind2 I ⇒ ⓑ{I} (fsubst W d V). (fsubst W (d+1) T)
+  | Flat2 I ⇒ ⓕ{I} (fsubst W d V). (fsubst W d T)
   ]
 ].
 
@@ -34,7 +34,7 @@ interpretation "functional core substitution" 'Subst V d T = (fsubst V d T).
 (* Main properties **********************************************************)
 
 theorem fsubst_delift: ∀K,V,T,L,d.
-                       ⇩[0, d] L ≡ K. 𝕓{Abbr} V → L ⊢ T [d, 1] ≡ [d ← V] T.
+                       ⇩[0, d] L ≡ K. ⓓV → L ⊢ T [d, 1] ≡ [d ← V] T.
 #K #V #T elim T -T
 [ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/
   elim (lt_or_eq_or_gt i d) #Hid
@@ -48,7 +48,7 @@ qed.
 
 (* Main inversion properties ************************************************)
 
-theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. 𝕓{Abbr} V →
+theorem fsubst_inv_delift: ∀K,V,T1,L,T2,d. ⇩[0, d] L ≡ K. ⓓV →
                            L ⊢ T1 [d, 1] ≡ T2 → [d ← V] T1 = T2.
 #K #V #T1 elim T1 -T1
 [ * #i #L #T2 #d #HLK #H
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma
index 8062d8604..61a9666b5 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/aarity.ma
@@ -12,6 +12,14 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(* THE FORMAL SYSTEM λδ - MATITA SOURCE FILES
+ * Confluence of context-sensitive parallel reduction closed: 2011 September 21
+ * Confluence of context-free parallel reduction closed: 2011 September 6
+ * Specification started: 2011 April 17
+ * - Patience on me to gain peace and perfection! -
+ * [ suggested invocation to start formal specifications with ]
+ *)
+
 include "Ground_2/star.ma".
 include "Basic_2/notation.ma".
 
@@ -22,13 +30,15 @@ inductive aarity: Type[0] ≝
   | APair: aarity → aarity → aarity (* binary aarity construction *)
 .
 
-interpretation "aarity construction (atomic)" 'SItem = AAtom.
+interpretation "aarity construction (atomic)"
+   'Item0 = AAtom.
 
-interpretation "aarity construction (binary)" 'SItem A1 A2 = (APair A1 A2).
+interpretation "aarity construction (binary)"
+   'SnItem2 A1 A2 = (APair A1 A2).
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma discr_apair_xy_x: ∀A,B. 𝕔 B. A = B → False.
+lemma discr_apair_xy_x: ∀A,B. ②B. A = B → False.
 #A #B elim B -B
 [ #H destruct
 | #Y #X #IHY #_ #H destruct
@@ -37,7 +47,7 @@ lemma discr_apair_xy_x: ∀A,B. 𝕔 B. A = B → False.
 ]
 qed-.
 
-lemma discr_tpair_xy_y: ∀B,A. 𝕔 B. A = A → False.
+lemma discr_tpair_xy_y: ∀B,A. ②B. A = A → False.
 #B #A elim A -A
 [ #H destruct
 | #Y #X #_ #IHX #H destruct
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_shift.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_shift.ma
index c2fd85899..3a259cecf 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_shift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_shift.ma
@@ -18,7 +18,7 @@ include "Basic_2/grammar/lenv.ma".
 
 let rec shift L T on L ≝ match L with
 [ LAtom       ⇒ T
-| LPair L I V ⇒ shift L (𝕓{I} V. T)
+| LPair L I V ⇒ shift L (ⓑ{I} V. T)
 ].
 
 interpretation "shift (closure)" 'Append L T = (shift L T).
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
index 22818a980..925b84a34 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/cl_weight.ma
@@ -31,7 +31,7 @@ axiom cw_wf_ind: ∀R:lenv→predicate term.
                  ∀L,T. R L T.
 
 (* Basic_1: was: flt_shift *)
-lemma cw_shift: ∀K,I,V,T. #[K. 𝕓{I} V, T] < #[K, 𝕔{I} V. T].
+lemma cw_shift: ∀K,I,V,T. #[K. ⓑ{I} V, T] < #[K, ②{I} V. T].
 normalize //
 qed.
 
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/genv.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/genv.ma
index dad4fd230..349f8708a 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/genv.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/genv.ma
@@ -23,8 +23,17 @@ definition genv ≝ list2 bind2 term.
 interpretation "sort (global environment)"
    'Star = (nil2 bind2 term).
 
+interpretation "environment construction (binary)"
+   'DxItem2 L I T = (cons2 bind2 term I T L).
+
 interpretation "environment binding construction (binary)"
-   'DBind L I T = (cons2 bind2 term I T L).
+   'DxBind2 L I T = (cons2 bind2 term I T L).
+
+interpretation "abbreviation (global environment)"
+   'DxAbbr L T = (cons2 bind2 term Abbr T L).
+
+interpretation "abstraction (global environment)"
+   'DxAbst L T = (cons2 bind2 term Abst T L).
 
 (* Basic properties *********************************************************)
 
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma
index 08e35083d..89f1a94e4 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/item.ma
@@ -12,14 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* THE FORMAL SYSTEM λδ - MATITA SOURCE FILES
- * Confluence of context-sensitive parallel reduction closed: 2011 September 21
- * Confluence of context-free parallel reduction closed: 2011 September 6
- * Specification started: 2011 April 17
- * - Patience on me to gain peace and perfection! -
- * [ suggested invocation to start formal specifications with ]
- *)
-
 include "Ground_2/arith.ma".
 include "Basic_2/notation.ma".
 
@@ -46,13 +38,13 @@ inductive flat2: Type[0] ≝
 
 (* binary items *)
 inductive item2: Type[0] ≝
-  | Bind: bind2 → item2 (* binding item *)
-  | Flat: flat2 → item2 (* non-binding item *)
+  | Bind2: bind2 → item2 (* binding item *)
+  | Flat2: flat2 → item2 (* non-binding item *)
 .
 
-coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind on _I:bind2 to item2.
+coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind2 on _I:bind2 to item2.
 
-coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat on _I:flat2 to item2.
+coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat2 on _I:flat2 to item2.
 
 (* Basic properties *********************************************************)
 
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv.ma
index 15ca1ed17..5aacaf57c 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lenv.ma
@@ -22,6 +22,17 @@ inductive lenv: Type[0] ≝
 | LPair: lenv → bind2 → term → lenv (* binary binding construction *)
 .
 
-interpretation "sort (local environment)" 'Star = LAtom.
+interpretation "sort (local environment)"
+   'Star = LAtom.
 
-interpretation "environment binding construction (binary)" 'DBind L I T = (LPair L I T).
+interpretation "environment construction (binary)"
+   'DxItem2 L I T = (LPair L I T).
+
+interpretation "environment binding construction (binary)"
+   'DxBind2 L I T = (LPair L I T).
+
+interpretation "abbreviation (local environment)"
+   'DxAbbr L T = (LPair L Abbr T).
+
+interpretation "abstraction (local environment)"
+   'DxAbst L T = (LPair L Abst T).
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma
index 6f3ec1513..2c27f0f9e 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/lsubs.ma
@@ -20,11 +20,11 @@ inductive lsubs: nat → nat → relation lenv ≝
 | lsubs_sort: ∀d,e. lsubs d e (⋆) (⋆)
 | lsubs_OO:   ∀L1,L2. lsubs 0 0 L1 L2
 | lsubs_abbr: ∀L1,L2,V,e. lsubs 0 e L1 L2 →
-              lsubs 0 (e + 1) (L1. 𝕓{Abbr} V) (L2.𝕓{Abbr} V)
+              lsubs 0 (e + 1) (L1. ⓓV) (L2.ⓓV)
 | lsubs_abst: ∀L1,L2,I,V1,V2,e. lsubs 0 e L1 L2 →
-              lsubs 0 (e + 1) (L1. 𝕓{Abst} V1) (L2.𝕓{I} V2)
+              lsubs 0 (e + 1) (L1. ⓛV1) (L2.ⓑ{I} V2)
 | lsubs_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
-              lsubs d e L1 L2 → lsubs (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2)
+              lsubs d e L1 L2 → lsubs (d + 1) e (L1. ⓑ{I1} V1) (L2. ⓑ{I2} V2)
 .
 
 interpretation
@@ -46,7 +46,7 @@ lemma TC_lsubs_conf: ∀S,R. lsubs_conf S R → lsubs_conf S (λL. (TC … (R L)
 qed.
 
 lemma lsubs_bind_eq: ∀L1,L2,e. L1 [0, e] ≼ L2 → ∀I,V.
-                     L1. 𝕓{I} V [0, e + 1] ≼ L2.𝕓{I} V.
+                     L1. ⓑ{I} V [0, e + 1] ≼ L2.ⓑ{I} V.
 #L1 #L2 #e #HL12 #I #V elim I -I /2 width=1/
 qed.
 
@@ -58,7 +58,7 @@ lemma lsubs_refl: ∀d,e,L. L [d, e] ≼ L.
 qed.
 
 lemma lsubs_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≼ L2 → 0 < d →
-                     ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≼ L2. 𝕓{I2} V2.
+                     ∀I1,I2,V1,V2. L1. ⓑ{I1} V1 [d, e] ≼ L2. ⓑ{I2} V2.
 
 #L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) // /2 width=1/
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma
index 42e7b8633..d66a9c520 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term.ma
@@ -22,23 +22,42 @@ inductive term: Type[0] ≝
   | TPair: item2 → term → term → term (* binary item construction *)
 .
 
-interpretation "sort (term)" 'Star k = (TAtom (Sort k)).
+interpretation "term construction (atomic)"
+   'Item0 I = (TAtom I).
 
-interpretation "local reference (term)" 'LRef i = (TAtom (LRef i)).
+interpretation "term construction (binary)"
+   'SnItem2 I T1 T2 = (TPair I T1 T2).
 
-interpretation "global reference (term)" 'GRef p = (TAtom (GRef p)).
+interpretation "term binding construction (binary)"
+   'SnBind2 I T1 T2 = (TPair (Bind2 I) T1 T2).
 
-interpretation "term construction (atomic)" 'SItem I = (TAtom I).
+interpretation "term flat construction (binary)"
+   'SnFlat2 I T1 T2 = (TPair (Flat2 I) T1 T2).
 
-interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2).
+interpretation "sort (term)"
+   'Star k = (TAtom (Sort k)).
 
-interpretation "term binding construction (binary)" 'SBind I T1 T2 = (TPair (Bind I) T1 T2).
+interpretation "local reference (term)"
+   'LRef i = (TAtom (LRef i)).
 
-interpretation "term flat construction (binary)" 'SFlat I T1 T2 = (TPair (Flat I) T1 T2).
+interpretation "global reference (term)"
+   'GRef p = (TAtom (GRef p)).
+
+interpretation "abbreviation (term)"
+   'SnAbbr T1 T2 = (TPair (Bind2 Abbr) T1 T2).
+
+interpretation "abstraction (term)"
+   'SnAbst T1 T2 = (TPair (Bind2 Abst) T1 T2).
+
+interpretation "application (term)"
+   'SnAppl T1 T2 = (TPair (Flat2 Appl) T1 T2).
+
+interpretation "native type annotation (term)"
+   'SnCast T1 T2 = (TPair (Flat2 Cast) T1 T2).
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma discr_tpair_xy_x: ∀I,T,V. 𝕔{I} V. T = V → False.
+lemma discr_tpair_xy_x: ∀I,T,V. ②{I} V. T = V → False.
 #I #T #V elim V -V
 [ #J #H destruct
 | #J #W #U #IHW #_ #H destruct
@@ -48,7 +67,7 @@ lemma discr_tpair_xy_x: ∀I,T,V. 𝕔{I} V. T = V → False.
 qed-.
 
 (* Basic_1: was: thead_x_y_y *)
-lemma discr_tpair_xy_y: ∀I,V,T. 𝕔{I} V. T = T → False.
+lemma discr_tpair_xy_y: ∀I,V,T. ②{I} V. T = T → False.
 #I #V #T elim T -T
 [ #J #H destruct
 | #J #W #U #_ #IHU #H destruct
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma
index be4811eeb..8f7c70374 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_simple.ma
@@ -17,20 +17,20 @@ include "Basic_2/grammar/term.ma".
 (* SIMPLE (NEUTRAL) TERMS ***************************************************)
 
 inductive simple: predicate term ≝
-   | simple_atom: ∀I. simple (𝕒{I})
-   | simple_flat: ∀I,V,T. simple (𝕗{I} V. T)
+   | simple_atom: ∀I. simple (⓪{I})
+   | simple_flat: ∀I,V,T. simple (ⓕ{I} V. T)
 .
 
 interpretation "simple (term)" 'Simple T = (simple T).
 
 (* Basic inversion lemmas ***************************************************)
 
-fact simple_inv_bind_aux: ∀T. 𝕊[T] → ∀J,W,U. T = 𝕓{J} W. U → False.
+fact simple_inv_bind_aux: ∀T. 𝕊[T] → ∀J,W,U. T = ⓑ{J} W. U → False.
 #T * -T
 [ #I #J #W #U #H destruct
 | #I #V #T #J #W #U #H destruct
 ]
 qed.
 
-lemma simple_inv_bind: ∀I,V,T. 𝕊[𝕓{I} V. T] → False.
+lemma simple_inv_bind: ∀I,V,T. 𝕊[ⓑ{I} V. T] → False.
 /2 width=6/ qed-.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma
index 01dec2102..2b3f8880e 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma
@@ -20,7 +20,8 @@ include "Basic_2/grammar/term.ma".
 let rec applv Vs T on Vs ≝
   match Vs with
   [ nil        ⇒ T
-  | cons hd tl ⇒  𝕔{Appl} hd. (applv tl T)
+  | cons hd tl ⇒  ⓐhd. (applv tl T)
   ].
 
-interpretation "application construction (vector)" 'ApplV Vs T = (applv Vs T).
+interpretation "application o vevtor (term)"
+   'SnApplV Vs T = (applv Vs T).
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma
index aaade3b54..149b27a17 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/thom.ma
@@ -17,10 +17,10 @@ include "Basic_2/grammar/term_simple.ma".
 (* HOMOMORPHIC TERMS ********************************************************)
 
 inductive thom: relation term ≝
-   | thom_atom: ∀I. thom (𝕒{I}) (𝕒{I})
-   | thom_abst: ∀V1,V2,T1,T2. thom (𝕔{Abst} V1. T1) (𝕔{Abst} V2. T2)
+   | thom_atom: ∀I. thom (⓪{I}) (⓪{I})
+   | thom_abst: ∀V1,V2,T1,T2. thom (ⓛV1. T1) (ⓛV2. T2)
    | thom_appl: ∀V1,V2,T1,T2. thom T1 T2 → 𝕊[T1] → 𝕊[T2] →
-                thom (𝕔{Appl} V1. T1) (𝕔{Appl} V2. T2)
+                thom (ⓐV1. T1) (ⓐV2. T2)
 .
 
 interpretation "homomorphic (term)" 'napart T1 T2 = (thom T1 T2).
@@ -49,8 +49,8 @@ lemma simple_thom_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝕊[T2] → 𝕊[T1].
 
 (* Basic inversion lemmas ***************************************************)
 
-fact thom_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = 𝕓{I}W1.U1 →
-                         ∃∃W2,U2. I = Abst & T2 = 𝕔{Abst} W2. U2.
+fact thom_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓑ{I}W1.U1 →
+                         ∃∃W2,U2. I = Abst & T2 = ⓛW2. U2.
 #T1 #T2 * -T1 -T2
 [ #J #I #W1 #U1 #H destruct
 | #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3/
@@ -58,13 +58,13 @@ fact thom_inv_bind1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = 𝕓{I}W1.U1 
 ]
 qed.
 
-lemma thom_inv_bind1: ∀I,W1,U1,T2. 𝕓{I}W1.U1 ≈ T2 →
-                      ∃∃W2,U2. I = Abst & T2 = 𝕔{Abst} W2. U2.
+lemma thom_inv_bind1: ∀I,W1,U1,T2. ⓑ{I}W1.U1 ≈ T2 →
+                      ∃∃W2,U2. I = Abst & T2 = ⓛW2. U2.
 /2 width=5/ qed-.
 
-fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = 𝕗{I}W1.U1 →
+fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = ⓕ{I}W1.U1 →
                          ∃∃W2,U2. U1 ≈ U2 & 𝕊[U1] & 𝕊[U2] &
-                                  I = Appl & T2 = 𝕔{Appl} W2. U2.
+                                  I = Appl & T2 = ⓐW2. U2.
 #T1 #T2 * -T1 -T2
 [ #J #I #W1 #U1 #H destruct
 | #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct
@@ -72,9 +72,9 @@ fact thom_inv_flat1_aux: ∀T1,T2. T1 ≈ T2 → ∀I,W1,U1. T1 = 𝕗{I}W1.U1 
 ]
 qed.
 
-lemma thom_inv_flat1: ∀I,W1,U1,T2. 𝕗{I}W1.U1 ≈ T2 →
+lemma thom_inv_flat1: ∀I,W1,U1,T2. ⓕ{I}W1.U1 ≈ T2 →
                       ∃∃W2,U2. U1 ≈ U2 & 𝕊[U1] & 𝕊[U2] &
-                               I = Appl & T2 = 𝕔{Appl} W2. U2.
+                               I = Appl & T2 = ⓐW2. U2.
 /2 width=4/ qed-.
 
 (* Basic_1: removed theorems 7:
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/names.txt b/matita/matita/contribs/lambda_delta/Basic_2/names.txt
index a57d3affb..cc9bb6936 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/names.txt
+++ b/matita/matita/contribs/lambda_delta/Basic_2/names.txt
@@ -23,3 +23,17 @@ i,j    : local reference position index (de Bruijn's)
 k      : sort index
 p,q    : global reference position
 t,u    : local reference position level (de Bruijn's)
+
+NAMING CONVENTIONS FOR CONSTRUCTORS
+
+0: atomic
+2: binary
+
+A: application to vector
+
+a: application
+b: binder
+d: abbreviation
+f: flat
+l: abstraction
+t: native type annotation
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
index db2b5622c..f10f7b4f6 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/notation.ma
@@ -16,6 +16,14 @@
 
 (* Grammar ******************************************************************)
 
+notation "hvbox( ⓪ )"
+ non associative with precedence 90
+ for @{ 'Item0 }.
+
+notation "hvbox( ⓪ { I } )"
+ non associative with precedence 90
+ for @{ 'Item0 $I }.
+
 notation "hvbox( ⋆ )"
  non associative with precedence 90
  for @{ 'Star }.
@@ -32,45 +40,61 @@ notation "hvbox( § term 90 p )"
  non associative with precedence 90
  for @{ 'GRef $p }.
 
-notation "hvbox( 𝕒 )"
+notation "hvbox( ② term 90 T1 . break term 90 T )"
  non associative with precedence 90
- for @{ 'SItem }.
+ for @{ 'SnItem2 $T1 $T }.
 
-notation "hvbox( 𝕒 { I } )"
+notation "hvbox( ② { I } break term 90 T1 . break term 90 T )"
  non associative with precedence 90
- for @{ 'SItem $I }.
+ for @{ 'SnItem2 $I $T1 $T }.
 
-notation "hvbox( 𝕔 term 90 T1 . break term 90 T )"
+notation "hvbox( ⓑ { I } break term 90 T1 . break term 90 T )"
  non associative with precedence 90
- for @{ 'SItem $T1 $T }.
+ for @{ 'SnBind2 $I $T1 $T }.
 
-notation "hvbox( 𝕔 { I } break term 90 T1 . break term 90 T )"
+notation "hvbox( ⓕ { I } break term 90 T1 . break term 90 T )"
  non associative with precedence 90
- for @{ 'SItem $I $T1 $T }.
+ for @{ 'SnFlat2 $I $T1 $T }.
 
-notation "hvbox( 𝕓 { I } break term 90 T1 . break term 90 T )"
+notation "hvbox( ⓓ  term 90 T1 . break term 90 T2 )"
  non associative with precedence 90
- for @{ 'SBind $I $T1 $T }.
+ for @{ 'SnAbbr $T1 $T2 }.
 
-notation "hvbox( 𝕗 { I } break term 90 T1 . break term 90 T )"
+notation "hvbox( ⓛ  term 90 T1 . break term 90 T2 )"
  non associative with precedence 90
- for @{ 'SFlat $I $T1 $T }.
+ for @{ 'SnAbst $T1 $T2 }.
+
+notation "hvbox( ⓐ  term 90 T1 . break term 90 T2 )"
+ non associative with precedence 90
+ for @{ 'SnAppl $T1 $T2 }.
+
+notation "hvbox( ⓣ  term 90 T1 . break term 90 T2 )"
+ non associative with precedence 90
+ for @{ 'SnCast $T1 $T2 }.
 
 notation "hvbox( Ⓐ term 90 T1 . break term 90 T )"
  non associative with precedence 90
- for @{ 'ApplV $T1 $T }.
+ for @{ 'SnApplV $T1 $T }.
 
-notation "hvbox( T . break 𝕓 { I } break term 90 T1 )"
- non associative with precedence 89
- for @{ 'DBind $T $I $T1 }.
-(*
-notation > "hvbox( T . break 𝕔 { I } break term 90 T1 )"
+notation > "hvbox( T . break ②{ I } break term 47 T1 )"
+ non associative with precedence 46
+ for @{ 'DxBind2 $T $I $T1 }.
+
+notation "hvbox( T . break ⓑ { I } break term 90 T1 )"
  non associative with precedence 89
- for @{ 'DBind $T $I $T1 }.
-*) (**) (* this breaks all parsing *)
+ for @{ 'DxBind2 $T $I $T1 }.
+
+notation "hvbox( T1 . break ⓓ T2 )"
+ left associative with precedence 48
+ for @{ 'DxAbbr $T1 $T2 }.
+
+notation "hvbox( T1 . break ⓛ T2 )"
+ left associative with precedence 49
+ for @{ 'DxAbst $T1 $T2 }.
+
 notation "hvbox( T . break ④ { I } break { T1 , break T2 , break T3 } )"
  non associative with precedence 47
- for @{ 'DBind $T $I $T1 $T2 $T3 }.
+ for @{ 'DxItem4 $T $I $T1 $T2 $T3 }.
 
 notation "hvbox( # [ x ] )"
  non associative with precedence 90
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma
index bcc50fa6e..b3812e942 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr.ma
@@ -41,12 +41,12 @@ lemma cpr_refl: ∀L,T. L ⊢ T ➡ T.
 (* Note: new property *)
 (* Basic_1: was only: pr2_thin_dx *) 
 lemma cpr_flat: ∀I,L,V1,V2,T1,T2.
-                L ⊢ V1 ➡ V2 → L ⊢ T1 ➡ T2 → L ⊢ 𝕗{I} V1. T1 ➡ 𝕗{I} V2. T2.
+                L ⊢ V1 ➡ V2 → L ⊢ T1 ➡ T2 → L ⊢ ⓕ{I} V1. T1 ➡ ⓕ{I} V2. T2.
 #I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 * /3 width=5/
 qed.
 
 lemma cpr_cast: ∀L,V,T1,T2.
-                L ⊢ T1 ➡ T2 → L ⊢ 𝕔{Cast} V. T1 ➡ T2.
+                L ⊢ T1 ➡ T2 → L ⊢ ⓣV. T1 ➡ T2.
 #L #V #T1 #T2 * /3 width=3/
 qed.
 
@@ -74,9 +74,9 @@ lemma cpr_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ➡ T2 → T2 = ⋆k.
 qed-.
 
 (* Basic_1: was: pr2_gen_cast *)
-lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ 𝕔{Cast} V1. T1 ➡ U2 → (
+lemma cpr_inv_cast1: ∀L,V1,T1,U2. L ⊢ ⓣV1. T1 ➡ U2 → (
                         ∃∃V2,T2. L ⊢ V1 ➡ V2 & L ⊢ T1 ➡ T2 &
-                                 U2 = 𝕔{Cast} V2. T2
+                                 U2 = ⓣV2. T2
                      ) ∨ L ⊢ T1 ➡ U2.
 #L #V1 #T1 #U2 * #X #H #HU2
 elim (tpr_inv_cast1 … H) -H /3 width=3/
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma
index 553cde83a..555344994 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_cpr.ma
@@ -20,17 +20,17 @@ include "Basic_2/reducibility/cpr.ma".
 (* Advanced properties ******************************************************)
 
 lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ➡ V2 → T1 ➡ T2 →
-                   L ⊢ 𝕓{I} V1. T1 ➡ 𝕓{I} V2. T2.
+                   L ⊢ ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2.
 #I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12 
 @ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2 width=3/ (* /3 width=5/ is too slow *)
 qed.
 
 (* Basic_1: was only: pr2_gen_cbind *)
-lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ➡ V2 → L. 𝕓{I} V2 ⊢ T1 ➡ T2 →
-                   L ⊢ 𝕓{I} V1. T1 ➡ 𝕓{I} V2. T2.
+lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ➡ V2 → L. ⓑ{I} V2 ⊢ T1 ➡ T2 →
+                   L ⊢ ⓑ{I} V1. T1 ➡ ⓑ{I} V2. T2.
 #I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2
 elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
-lapply (tpss_lsubs_conf … HT0 (⋆. 𝕓{I} V2) ?) -HT0 /2 width=1/ #HT0
+lapply (tpss_lsubs_conf … HT0 (⋆. ⓑ{I} V2) ?) -HT0 /2 width=1/ #HT0
 lapply (tpss_tps … HT0) -HT0 #HT0
 @ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *)
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma
index 5f800c994..fcdcdcdd8 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/cpr_lift.ma
@@ -21,7 +21,7 @@ include "Basic_2/reducibility/cpr.ma".
 (* Advanced properties ******************************************************)
 
 lemma cpr_cdelta: ∀L,K,V1,W1,W2,i.
-                  ⇩[0, i] L ≡ K. 𝕓{Abbr} V1 → K ⊢ V1 [0, |L| - i - 1] ▶* W1 →
+                  ⇩[0, i] L ≡ K. ⓓV1 → K ⊢ V1 [0, |L| - i - 1] ▶* W1 →
                   ⇧[0, i + 1] W1 ≡ W2 → L ⊢ #i ➡ W2.
 #L #K #V1 #W1 #W2 #i #HLK #HVW1 #HW12
 lapply (ldrop_fwd_ldrop2_length … HLK) #Hi
@@ -33,7 +33,7 @@ qed.
 (* Basic_1: was: pr2_gen_lref *)
 lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ➡ T2 →
                      T2 = #i ∨
-                     ∃∃K,V1,T1. ⇩[0, i] L ≡ K. 𝕓{Abbr} V1 &
+                     ∃∃K,V1,T1. ⇩[0, i] L ≡ K. ⓓV1 &
                                 K ⊢ V1 [0, |L| - i - 1] ▶* T1 &
                                 ⇧[0, i + 1] T1 ≡ T2 &
                                 i < |L|.
@@ -44,8 +44,8 @@ elim (tpss_inv_lref1 … H) -H /2 width=1/
 qed-.
 
 (* Basic_1: was: pr2_gen_abst *)
-lemma cpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ➡ U2 →
-                     ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = 𝕔{Abst} V2. T2.
+lemma cpr_inv_abst1: ∀V1,T1,U2. ⓛV1. T1 ➡ U2 →
+                     ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓛV2. T2.
 /2 width=3/ qed-.
 
 (* Relocation properties ****************************************************)
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma
index 3675669c3..8e834b2da 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/ltpr.ma
@@ -19,7 +19,7 @@ include "Basic_2/reducibility/tpr.ma".
 inductive ltpr: relation lenv ≝
 | ltpr_stom: ltpr (⋆) (⋆)
 | ltpr_pair: ∀K1,K2,I,V1,V2.
-             ltpr K1 K2 → V1 ➡ V2 → ltpr (K1. 𝕓{I} V1) (K2. 𝕓{I} V2) (*𝕓*)
+             ltpr K1 K2 → V1 ➡ V2 → ltpr (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) (*ⓑ*)
 .
 
 interpretation
@@ -45,8 +45,8 @@ qed.
 lemma ltpr_inv_atom1: ∀L2. ⋆ ➡ L2 → L2 = ⋆.
 /2 width=3/ qed-.
 
-fact ltpr_inv_pair1_aux: ∀L1,L2. L1 ➡ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
-                         ∃∃K2,V2. K1 ➡ K2 & V1 ➡ V2 & L2 = K2. 𝕓{I} V2.
+fact ltpr_inv_pair1_aux: ∀L1,L2. L1 ➡ L2 → ∀K1,I,V1. L1 = K1. ⓑ{I} V1 →
+                         ∃∃K2,V2. K1 ➡ K2 & V1 ➡ V2 & L2 = K2. ⓑ{I} V2.
 #L1 #L2 * -L1 -L2
 [ #K1 #I #V1 #H destruct
 | #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct /2 width=5/
@@ -54,8 +54,8 @@ fact ltpr_inv_pair1_aux: ∀L1,L2. L1 ➡ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1
 qed.
 
 (* Basic_1: was: wcpr0_gen_head *)
-lemma ltpr_inv_pair1: ∀K1,I,V1,L2. K1. 𝕓{I} V1 ➡ L2 →
-                      ∃∃K2,V2. K1 ➡ K2 & V1 ➡ V2 & L2 = K2. 𝕓{I} V2.
+lemma ltpr_inv_pair1: ∀K1,I,V1,L2. K1. ⓑ{I} V1 ➡ L2 →
+                      ∃∃K2,V2. K1 ➡ K2 & V1 ➡ V2 & L2 = K2. ⓑ{I} V2.
 /2 width=3/ qed-.
 
 fact ltpr_inv_atom2_aux: ∀L1,L2. L1 ➡ L2 → L2 = ⋆ → L1 = ⋆.
@@ -68,16 +68,16 @@ qed.
 lemma ltpr_inv_atom2: ∀L1. L1 ➡ ⋆ → L1 = ⋆.
 /2 width=3/ qed-.
 
-fact ltpr_inv_pair2_aux: ∀L1,L2. L1 ➡ L2 → ∀K2,I,V2. L2 = K2. 𝕓{I} V2 →
-                         ∃∃K1,V1. K1 ➡ K2 & V1 ➡ V2 & L1 = K1. 𝕓{I} V1.
+fact ltpr_inv_pair2_aux: ∀L1,L2. L1 ➡ L2 → ∀K2,I,V2. L2 = K2. ⓑ{I} V2 →
+                         ∃∃K1,V1. K1 ➡ K2 & V1 ➡ V2 & L1 = K1. ⓑ{I} V1.
 #L1 #L2 * -L1 -L2
 [ #K2 #I #V2 #H destruct
 | #K1 #K2 #I #V1 #V2 #HK12 #HV12 #K #J #W #H destruct /2 width=5/
 ]
 qed.
 
-lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ➡ K2. 𝕓{I} V2 →
-                      ∃∃K1,V1. K1 ➡ K2 & V1 ➡ V2 & L1 = K1. 𝕓{I} V1.
+lemma ltpr_inv_pair2: ∀L1,K2,I,V2. L1 ➡ K2. ⓑ{I} V2 →
+                      ∃∃K1,V1. K1 ➡ K2 & V1 ➡ V2 & L1 = K1. ⓑ{I} V1.
 /2 width=3/ qed-.
 
 (* Basic forward lemmas *****************************************************)
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma
index 83ca7d0af..3c0184e55 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tnf.ma
@@ -26,36 +26,36 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma tnf_inv_abst: ∀V,T. ℕ[𝕔{Abst}V.T] → ℕ[V] ∧ ℕ[T].
+lemma tnf_inv_abst: ∀V,T. ℕ[ⓛV.T] → ℕ[V] ∧ ℕ[T].
 #V1 #T1 #HVT1 @conj
-[ #V2 #HV2 lapply (HVT1 (𝕔{Abst}V2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (𝕔{Abst}V1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (ⓛV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓛV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
 ]
 qed-.
 
-lemma tnf_inv_appl: ∀V,T. ℕ[𝕔{Appl}V.T] → ∧∧ ℕ[V] & ℕ[T] & 𝕊[T].
+lemma tnf_inv_appl: ∀V,T. ℕ[ⓐV.T] → ∧∧ ℕ[V] & ℕ[T] & 𝕊[T].
 #V1 #T1 #HVT1 @and3_intro
-[ #V2 #HV2 lapply (HVT1 (𝕔{Appl}V2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
-| #T2 #HT2 lapply (HVT1 (𝕔{Appl}V1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
+[ #V2 #HV2 lapply (HVT1 (ⓐV2.T1) ?) -HVT1 /2 width=1/ -HV2 #H destruct //
+| #T2 #HT2 lapply (HVT1 (ⓐV1.T2) ?) -HVT1 /2 width=1/ -HT2 #H destruct //
 | generalize in match HVT1; -HVT1 elim T1 -T1 * // * #W1 #U1 #_ #_ #H
   [ elim (lift_total V1 0 1) #V2 #HV12
-    lapply (H (𝕔{Abbr}W1.𝕔{Appl}V2.U1) ?) -H /2 width=3/ -HV12 #H destruct
-  | lapply (H (𝕔{Abbr}V1.U1) ?) -H /2 width=1/ #H destruct
+    lapply (H (ⓓW1.ⓐV2.U1) ?) -H /2 width=3/ -HV12 #H destruct
+  | lapply (H (ⓓV1.U1) ?) -H /2 width=1/ #H destruct
 ]
 qed-.
 
-lemma tnf_inv_abbr: ∀V,T. ℕ[𝕔{Abbr}V.T] → False.
+lemma tnf_inv_abbr: ∀V,T. ℕ[ⓓV.T] → False.
 #V #T #H elim (is_lift_dec T 0 1)
 [ * #U #HTU
   lapply (H U ?) -H /2 width=3/ #H destruct
   elim (lift_inv_pair_xy_y … HTU)
 | #HT
-  elim (tps_full (⋆) V T (⋆. 𝕓{Abbr} V) 0 ?) // #T2 #T1 #HT2 #HT12
-  lapply (H (𝕓{Abbr}V.T2) ?) -H /2 width=3/ -HT2 #H destruct /3 width=2/
+  elim (tps_full (⋆) V T (⋆. ⓓV) 0 ?) // #T2 #T1 #HT2 #HT12
+  lapply (H (ⓓV.T2) ?) -H /2 width=3/ -HT2 #H destruct /3 width=2/
 ]
 qed.
 
-lemma tnf_inv_cast: ∀V,T. ℕ[𝕔{Cast}V.T] → False.
+lemma tnf_inv_cast: ∀V,T. ℕ[ⓣV.T] → False.
 #V #T #H lapply (H T ?) -H /2 width=1/ #H
 @(discr_tpair_xy_y … H)
 qed-.
@@ -109,8 +109,8 @@ qed.
 theorem tnf_tif: ∀T1. ℕ[T1] → 𝕀[T1].
 /2 width=3/ qed.
 
-lemma tnf_abst: ∀V,T. ℕ[V] → ℕ[T] → ℕ[𝕔{Abst}V.T].
+lemma tnf_abst: ∀V,T. ℕ[V] → ℕ[T] → ℕ[ⓛV.T].
 /4 width=1/ qed.
 
-lemma tnf_appl: ∀V,T. ℕ[V] → ℕ[T] → 𝕊[T] → ℕ[𝕔{Appl}V.T].
+lemma tnf_appl: ∀V,T. ℕ[V] → ℕ[T] → 𝕊[T] → ℕ[ⓐV.T].
 /4 width=1/ qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma
index 12aa95df6..c2508c851 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr.ma
@@ -18,21 +18,19 @@ include "Basic_2/substitution/tps.ma".
 
 (* Basic_1: includes: pr0_delta1 *)
 inductive tpr: relation term ≝
-| tpr_atom : ∀I. tpr (𝕒{I}) (𝕒{I})
+| tpr_atom : ∀I. tpr (⓪{I}) (⓪{I})
 | tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
-             tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2)
+             tpr (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
 | tpr_beta : ∀V1,V2,W,T1,T2.
-             tpr V1 V2 → tpr T1 T2 →
-             tpr (𝕔{Appl} V1. 𝕔{Abst} W. T1) (𝕔{Abbr} V2. T2)
+             tpr V1 V2 → tpr T1 T2 → tpr (ⓐV1. ⓛW. T1) (ⓓV2. T2)
 | tpr_delta: ∀I,V1,V2,T1,T2,T.
-             tpr V1 V2 → tpr T1 T2 → ⋆.  𝕓{I} V2 ⊢ T2 [0, 1] ▶ T →
-             tpr (𝕓{I} V1. T1) (𝕓{I} V2. T)
+             tpr V1 V2 → tpr T1 T2 → ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T →
+             tpr (ⓑ{I} V1. T1) (ⓑ{I} V2. T)
 | tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
              tpr V1 V2 → ⇧[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
-             tpr (𝕔{Appl} V1. 𝕔{Abbr} W1. T1) (𝕔{Abbr} W2. 𝕔{Appl} V. T2)
-| tpr_zeta : ∀V,T,T1,T2. ⇧[0,1] T1 ≡ T → tpr T1 T2 →
-             tpr (𝕔{Abbr} V. T) T2
-| tpr_tau  : ∀V,T1,T2. tpr T1 T2 → tpr (𝕔{Cast} V. T1) T2
+             tpr (ⓐV1. ⓓW1. T1) (ⓓW2. ⓐV. T2)
+| tpr_zeta : ∀V,T,T1,T2. ⇧[0,1] T1 ≡ T → tpr T1 T2 → tpr (ⓓV. T) T2
+| tpr_tau  : ∀V,T1,T2. tpr T1 T2 → tpr (ⓣV. T1) T2
 .
 
 interpretation
@@ -42,7 +40,7 @@ interpretation
 (* Basic properties *********************************************************)
 
 lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ➡ V2 → T1 ➡ T2 →
-                            𝕓{I} V1. T1 ➡  𝕓{I} V2. T2.
+                                ⓑ{I} V1. T1 ➡  ⓑ{I} V2. T2.
 /2 width=3/ qed.
 
 (* Basic_1: was by definition: pr0_refl *)
@@ -53,7 +51,7 @@ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-fact tpr_inv_atom1_aux: ∀U1,U2. U1 ➡ U2 → ∀I. U1 = 𝕒{I} → U2 = 𝕒{I}.
+fact tpr_inv_atom1_aux: ∀U1,U2. U1 ➡ U2 → ∀I. U1 = ⓪{I} → U2 = ⓪{I}.
 #U1 #U2 * -U1 -U2
 [ //
 | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
@@ -66,13 +64,13 @@ fact tpr_inv_atom1_aux: ∀U1,U2. U1 ➡ U2 → ∀I. U1 = 𝕒{I} → U2 = 𝕒
 qed.
 
 (* Basic_1: was: pr0_gen_sort pr0_gen_lref *)
-lemma tpr_inv_atom1: ∀I,U2. 𝕒{I} ➡ U2 → U2 = 𝕒{I}.
+lemma tpr_inv_atom1: ∀I,U2. ⓪{I} ➡ U2 → U2 = ⓪{I}.
 /2 width=3/ qed-.
 
-fact tpr_inv_bind1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
+fact tpr_inv_bind1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,T1. U1 = ⓑ{I} V1. T1 →
                         (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
-                                    ⋆.  𝕓{I} V2 ⊢ T2 [0, 1] ▶ T &
-                                    U2 = 𝕓{I} V2. T
+                                    ⋆.  ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T &
+                                    U2 = ⓑ{I} V2. T
                         ) ∨
                         ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr.
 #U1 #U2 * -U1 -U2
@@ -86,35 +84,35 @@ fact tpr_inv_bind1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1
 ]
 qed.
 
-lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ➡ U2 →
+lemma tpr_inv_bind1: ∀V1,T1,U2,I. ⓑ{I} V1. T1 ➡ U2 →
                      (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
-                                 ⋆.  𝕓{I} V2 ⊢ T2 [0, 1] ▶ T &
-                                 U2 = 𝕓{I} V2. T
+                                 ⋆.  ⓑ{I} V2 ⊢ T2 [0, 1] ▶ T &
+                                 U2 = ⓑ{I} V2. T
                      ) ∨
                      ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2 & I = Abbr.
 /2 width=3/ qed-.
 
 (* Basic_1: was pr0_gen_abbr *)
-lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ➡ U2 →
+lemma tpr_inv_abbr1: ∀V1,T1,U2. ⓓV1. T1 ➡ U2 →
                      (∃∃V2,T2,T. V1 ➡ V2 & T1 ➡ T2 &
-                                 ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ▶ T &
-                                 U2 = 𝕓{Abbr} V2. T
+                                 ⋆.  ⓓV2 ⊢ T2 [0, 1] ▶ T &
+                                 U2 = ⓓV2. T
                       ) ∨
                       ∃∃T. ⇧[0,1] T ≡ T1 & T ➡ U2.
 #V1 #T1 #U2 #H
 elim (tpr_inv_bind1 … H) -H * /3 width=7/
 qed-.
 
-fact tpr_inv_flat1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,U0. U1 = 𝕗{I} V1. U0 →
+fact tpr_inv_flat1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,U0. U1 = ⓕ{I} V1. U0 →
                         ∨∨ ∃∃V2,T2.            V1 ➡ V2 & U0 ➡ T2 &
-                                               U2 = 𝕗{I} V2. T2
+                                               U2 = ⓕ{I} V2. T2
                          | ∃∃V2,W,T1,T2.       V1 ➡ V2 & T1 ➡ T2 &
-                                               U0 = 𝕔{Abst} W. T1 &
-                                               U2 = 𝕔{Abbr} V2. T2 & I = Appl
+                                               U0 = ⓛW. T1 &
+                                               U2 = ⓓV2. T2 & I = Appl
                          | ∃∃V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
                                                ⇧[0,1] V2 ≡ V &
-                                               U0 = 𝕔{Abbr} W1. T1 &
-                                               U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
+                                               U0 = ⓓW1. T1 &
+                                               U2 = ⓓW2. ⓐV. T2 &
                                                I = Appl
                          |                     (U0 ➡ U2 ∧ I = Cast).
 #U1 #U2 * -U1 -U2
@@ -128,39 +126,39 @@ fact tpr_inv_flat1_aux: ∀U1,U2. U1 ➡ U2 → ∀I,V1,U0. U1 = 𝕗{I} V1. U0
 ]
 qed.
 
-lemma tpr_inv_flat1: ∀V1,U0,U2,I. 𝕗{I} V1. U0 ➡ U2 →
+lemma tpr_inv_flat1: ∀V1,U0,U2,I. ⓕ{I} V1. U0 ➡ U2 →
                      ∨∨ ∃∃V2,T2.            V1 ➡ V2 & U0 ➡ T2 &
-                                            U2 = 𝕗{I} V2. T2
+                                            U2 = ⓕ{I} V2. T2
                       | ∃∃V2,W,T1,T2.       V1 ➡ V2 & T1 ➡ T2 &
-                                            U0 = 𝕔{Abst} W. T1 &
-                                            U2 = 𝕔{Abbr} V2. T2 & I = Appl
+                                            U0 = ⓛW. T1 &
+                                            U2 = ⓓV2. T2 & I = Appl
                       | ∃∃V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
                                             ⇧[0,1] V2 ≡ V &
-                                            U0 = 𝕔{Abbr} W1. T1 &
-                                            U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
+                                            U0 = ⓓW1. T1 &
+                                            U2 = ⓓW2. ⓐV. T2 &
                                             I = Appl
                       |                     (U0 ➡ U2 ∧ I = Cast).
 /2 width=3/ qed-.
 
 (* Basic_1: was pr0_gen_appl *)
-lemma tpr_inv_appl1: ∀V1,U0,U2. 𝕔{Appl} V1. U0 ➡ U2 →
+lemma tpr_inv_appl1: ∀V1,U0,U2. ⓐV1. U0 ➡ U2 →
                      ∨∨ ∃∃V2,T2.            V1 ➡ V2 & U0 ➡ T2 &
-                                            U2 = 𝕔{Appl} V2. T2
+                                            U2 = ⓐV2. T2
                       | ∃∃V2,W,T1,T2.       V1 ➡ V2 & T1 ➡ T2 &
-                                            U0 = 𝕔{Abst} W. T1 &
-                                            U2 = 𝕔{Abbr} V2. T2
+                                            U0 = ⓛW. T1 &
+                                            U2 = ⓓV2. T2
                       | ∃∃V2,V,W1,W2,T1,T2. V1 ➡ V2 & W1 ➡ W2 & T1 ➡ T2 &
                                             ⇧[0,1] V2 ≡ V &
-                                            U0 = 𝕔{Abbr} W1. T1 &
-                                            U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2.
+                                            U0 = ⓓW1. T1 &
+                                            U2 = ⓓW2. ⓐV. T2.
 #V1 #U0 #U2 #H
 elim (tpr_inv_flat1 … H) -H * /3 width=12/ #_ #H destruct
 qed-.
 
 (* Note: the main property of simple terms *)
-lemma tpr_inv_appl1_simple: ∀V1,T1,U. 𝕔{Appl} V1. T1 ➡ U → 𝕊[T1] →
+lemma tpr_inv_appl1_simple: ∀V1,T1,U. ⓐV1. T1 ➡ U → 𝕊[T1] →
                             ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 &
-                                     U = 𝕔{Appl} V2. T2.
+                                     U = ⓐV2. T2.
 #V1 #T1 #U #H #HT1
 elim (tpr_inv_appl1 … H) -H *
 [ /2 width=5/
@@ -172,8 +170,8 @@ elim (tpr_inv_appl1 … H) -H *
 qed-.
 
 (* Basic_1: was: pr0_gen_cast *)
-lemma tpr_inv_cast1: ∀V1,T1,U2. 𝕔{Cast} V1. T1 ➡ U2 →
-                       (∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = 𝕔{Cast} V2. T2)
+lemma tpr_inv_cast1: ∀V1,T1,U2. ⓣV1. T1 ➡ U2 →
+                       (∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓣV2. T2)
                      ∨ T1 ➡ U2.
 #V1 #T1 #U2 #H
 elim (tpr_inv_flat1 … H) -H * /3 width=5/
@@ -185,8 +183,8 @@ qed-.
 fact tpr_inv_lref2_aux: ∀T1,T2. T1 ➡ T2 → ∀i. T2 = #i →
                         ∨∨           T1 = #i
                          | ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
-                                     T1 = 𝕔{Abbr} V. T
-                         | ∃∃V,T.    T ➡ #i & T1 = 𝕔{Cast} V. T.
+                                     T1 = ⓓV. T
+                         | ∃∃V,T.    T ➡ #i & T1 = ⓣV. T.
 #T1 #T2 * -T1 -T2
 [ #I #i #H destruct /2 width=1/
 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
@@ -201,8 +199,8 @@ qed.
 lemma tpr_inv_lref2: ∀T1,i. T1 ➡ #i →
                      ∨∨           T1 = #i
                       | ∃∃V,T,T0. ⇧[O,1] T0 ≡ T & T0 ➡ #i &
-                                  T1 = 𝕔{Abbr} V. T
-                      | ∃∃V,T.    T ➡ #i & T1 = 𝕔{Cast} V. T.
+                                  T1 = ⓓV. T
+                      | ∃∃V,T.    T ➡ #i & T1 = ⓣV. T.
 /2 width=3/ qed-.
 
 (* Basic_1: removed theorems 3:
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma
index 91da5fabe..be40639a8 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_lift.ma
@@ -101,8 +101,8 @@ qed.
 
 (* Advanced inversion lemmas ************************************************)
 
-fact tpr_inv_abst1_aux: ∀U1,U2. U1 ➡ U2 → ∀V1,T1. U1 = 𝕔{Abst} V1. T1 →
-                        ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = 𝕔{Abst} V2. T2.
+fact tpr_inv_abst1_aux: ∀U1,U2. U1 ➡ U2 → ∀V1,T1. U1 = ⓛV1. T1 →
+                        ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓛV2. T2.
 #U1 #U2 * -U1 -U2
 [ #I #V #T #H destruct
 | #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
@@ -116,6 +116,6 @@ fact tpr_inv_abst1_aux: ∀U1,U2. U1 ➡ U2 → ∀V1,T1. U1 = 𝕔{Abst} V1. T1
 qed.
 
 (* Basic_1: was pr0_gen_abst *)
-lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ➡ U2 →
-                     ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = 𝕔{Abst} V2. T2.
+lemma tpr_inv_abst1: ∀V1,T1,U2. ⓛV1. T1 ➡ U2 →
+                     ∃∃V2,T2. V1 ➡ V2 & T1 ➡ T2 & U2 = ⓛV2. T2.
 /2 width=3/ qed-.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma
index d0243cfb7..b1e3f3c1b 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpr.ma
@@ -18,7 +18,7 @@ include "Basic_2/reducibility/tpr_tpss.ma".
 
 (* Confluence lemmas ********************************************************)
 
-fact tpr_conf_atom_atom: ∀I. ∃∃X. 𝕒{I} ➡ X & 𝕒{I} ➡ X.
+fact tpr_conf_atom_atom: ∀I. ∃∃X. ⓪{I} ➡ X & ⓪{I} ➡ X.
 /2 width=3/ qed.
 
 fact tpr_conf_flat_flat:
@@ -28,7 +28,7 @@ fact tpr_conf_flat_flat:
       ∃∃X. X1 ➡ X & X2 ➡ X
    ) →
    V0 ➡ V1 → V0 ➡ V2 → T0 ➡ T1 → T0 ➡ T2 →
-   ∃∃T0. 𝕗{I} V1. T1 ➡ T0 & 𝕗{I} V2. T2 ➡ T0.
+   ∃∃T0. ⓕ{I} V1. T1 ➡ T0 & ⓕ{I} V2. T2 ➡ T0.
 #I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
 elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
 elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=5/
@@ -41,8 +41,8 @@ fact tpr_conf_flat_beta:
       ∃∃X. X1 ➡ X & X2 ➡ X
    ) →
    V0 ➡ V1 → V0 ➡ V2 →
-   U0 ➡ T2 → 𝕔{Abst} W0. U0 ➡ T1 →
-   ∃∃X. 𝕔{Appl} V1. T1 ➡ X & 𝕔{Abbr} V2. T2 ➡ X.
+   U0 ➡ T2 → ⓛW0. U0 ➡ T1 →
+   ∃∃X. ⓐV1. T1 ➡ X & ⓓV2. T2 ➡ X.
 #V0 #V1 #T1 #V2 #W0 #U0 #T2 #IH #HV01 #HV02 #HT02 #H
 elim (tpr_inv_abst1 … H) -H #W1 #U1 #HW01 #HU01 #H destruct
 elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2
@@ -60,8 +60,8 @@ fact tpr_conf_flat_theta:
       ∃∃X. X1 ➡ X & X2 ➡ X
    ) →
    V0 ➡ V1 → V0 ➡ V2 → ⇧[O,1] V2 ≡ V →
-   W0 ➡ W2 → U0 ➡ U2 →  𝕔{Abbr} W0. U0 ➡ T1 →
-   ∃∃X. 𝕔{Appl} V1. T1 ➡ X & 𝕔{Abbr} W2. 𝕔{Appl} V. U2 ➡ X.
+   W0 ➡ W2 → U0 ➡ U2 →  ⓓW0. U0 ➡ T1 →
+   ∃∃X. ⓐV1. T1 ➡ X & ⓓW2. ⓐV. U2 ➡ X.
 #V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H
 elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #VV #HVV1 #HVV2
 elim (lift_total VV 0 1) #VVV #HVV
@@ -97,7 +97,7 @@ fact tpr_conf_flat_cast:
       ∃∃X. X1 ➡ X & X2 ➡ X
    ) →
    V0 ➡ V1 → T0 ➡ T1 → T0 ➡ X2 →
-   ∃∃X. 𝕔{Cast} V1. T1 ➡ X & X2 ➡ X.
+   ∃∃X. ⓣV1. T1 ➡ X & X2 ➡ X.
 #X2 #V0 #V1 #T0 #T1 #IH #_ #HT01 #HT02
 elim (IH … HT01 … HT02) -HT01 -HT02 -IH // /3 width=3/
 qed.
@@ -109,7 +109,7 @@ fact tpr_conf_beta_beta:
       ∃∃X. X1 ➡ X & X2 ➡ X
    ) →
    V0 ➡ V1 → V0 ➡ V2 → T0 ➡ T1 → T0 ➡ T2 →
-   ∃∃X. 𝕔{Abbr} V1. T1 ➡X & 𝕔{Abbr} V2. T2 ➡ X.
+   ∃∃X. ⓓV1. T1 ➡X & ⓓV2. T2 ➡ X.
 #W0 #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
 elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/
 elim (IH … HT01 … HT02) -HT01 -HT02 -IH /2 width=1/ /3 width=5/
@@ -123,9 +123,9 @@ fact tpr_conf_delta_delta:
       ∃∃X. X1 ➡ X & X2 ➡ X
    ) →
    V0 ➡ V1 → V0 ➡ V2 → T0 ➡ T1 → T0 ➡ T2 →
-   ⋆. 𝕓{I1} V1 ⊢ T1 [O, 1] ▶ TT1 →
-   ⋆. 𝕓{I1} V2 ⊢ T2 [O, 1] ▶ TT2 →
-   ∃∃X. 𝕓{I1} V1. TT1 ➡ X & 𝕓{I1} V2. TT2 ➡ X.
+   ⋆. ⓑ{I1} V1 ⊢ T1 [O, 1] ▶ TT1 →
+   ⋆. ⓑ{I1} V2 ⊢ T2 [O, 1] ▶ TT2 →
+   ∃∃X. ⓑ{I1} V1. TT1 ➡ X & ⓑ{I1} V2. TT2 ➡ X.
 #I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2
 elim (IH … HV01 … HV02) -HV01 -HV02 // #V #HV1 #HV2
 elim (IH … HT01 … HT02) -HT01 -HT02 -IH // #T #HT1 #HT2
@@ -141,9 +141,9 @@ fact tpr_conf_delta_zeta:
       ∀X1,X2. X0 ➡ X1 → X0 ➡ X2 →
       ∃∃X. X1 ➡ X & X2 ➡ X
    ) →
-   V0 ➡ V1 → T0 ➡ T1 → ⋆. 𝕓{Abbr} V1 ⊢ T1 [O,1] ▶ TT1 →
+   V0 ➡ V1 → T0 ➡ T1 → ⋆. ⓓV1 ⊢ T1 [O,1] ▶ TT1 →
    T2 ➡ X2 → ⇧[O, 1] T2 ≡ T0 →
-   ∃∃X. 𝕓{Abbr} V1. TT1 ➡ X & X2 ➡ X.
+   ∃∃X. ⓓV1. TT1 ➡ X & X2 ➡ X.
 #X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HTX2 #HTT20
 elim (tpr_inv_lift … HT01 … HTT20) -HT01 #TT2 #HTT21 #HTT2
 lapply (tps_inv_lift1_eq … HTT1 … HTT21) -HTT1 #HTT1 destruct
@@ -160,7 +160,7 @@ fact tpr_conf_theta_theta:
    ) →
    V0 ➡ V1 → V0 ➡ V2 → W0 ➡ W1 → W0 ➡ W2 → T0 ➡ T1 → T0 ➡ T2 →
    ⇧[O, 1] V1 ≡ VV1 → ⇧[O, 1] V2 ≡ VV2 →
-   ∃∃X. 𝕔{Abbr} W1. 𝕔{Appl} VV1. T1 ➡ X & 𝕔{Abbr} W2. 𝕔{Appl} VV2. T2 ➡ X.
+   ∃∃X. ⓓW1. ⓐVV1. T1 ➡ X & ⓓW2. ⓐVV2. T2 ➡ X.
 #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #V2 #VV2 #W2 #T2 #IH #HV01 #HV02 #HW01 #HW02 #HT01 #HT02 #HVV1 #HVV2
 elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2
 elim (IH … HW01 … HW02) -HW01 -HW02 /2 width=1/ #W #HW1 #HW2
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma
index 7fd1011c0..cf52701b5 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/tpr_tpss.ma
@@ -43,27 +43,27 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ➡ T2 →
   elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct
   elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct
   elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
-  elim (IHT12 … HTT1 (L2. 𝕓{Abst} WW) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
-  lapply (tpss_lsubs_conf … HTT2 (L2. 𝕓{Abbr} VV2) ?) -HTT2 /3 width=5/
+  elim (IHT12 … HTT1 (L2. ⓛWW) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
+  lapply (tpss_lsubs_conf … HTT2 (L2. ⓓVV2) ?) -HTT2 /3 width=5/
 | #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct
   elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
-  elim (IHT12 … HTT1 (L2. 𝕓{I} VV2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
+  elim (IHT12 … HTT1 (L2. ⓑ{I} VV2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
   elim (tpss_strip_neq … HTT2 … HTU2 ?) -T2 /2 width=1/ #T2 #HTT2 #HUT2
-  lapply (tps_lsubs_conf … HTT2 (L2. 𝕓{I} V2) ?) -HTT2 /2 width=1/ #HTT2
-  elim (ltpss_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) e ?) -HTT2 /2 width=1/ #W2 #HTTW2 #HTW2
-  lapply (tpss_lsubs_conf … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2 width=1/ #HTTW2
+  lapply (tps_lsubs_conf … HTT2 (L2. ⓑ{I} V2) ?) -HTT2 /2 width=1/ #HTT2
+  elim (ltpss_tps_conf … HTT2 (L2. ⓑ{I} VV2) (d + 1) e ?) -HTT2 /2 width=1/ #W2 #HTTW2 #HTW2
+  lapply (tpss_lsubs_conf … HTTW2 (⋆. ⓑ{I} VV2) ?) -HTTW2 /2 width=1/ #HTTW2
   lapply (tpss_tps … HTTW2) -HTTW2 #HTTW2
-  lapply (tpss_lsubs_conf … HTW2 (L2. 𝕓{I} VV2) ?) -HTW2 /2 width=1/ #HTW2
+  lapply (tpss_lsubs_conf … HTW2 (L2. ⓑ{I} VV2) ?) -HTW2 /2 width=1/ #HTW2
   lapply (tpss_trans_eq … HUT2 … HTW2) -T2 /3 width=5/
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct
   elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct
   elim (IHV12 … HVV1 … HL12) -V1 #VV2 #HVV12 #HVV2
   elim (IHW12 … HWW1 … HL12) -W1 #WW2 #HWW12 #HWW2
-  elim (IHT12 … HTT1 (L2. 𝕓{Abbr} WW2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
+  elim (IHT12 … HTT1 (L2. ⓓWW2) ?) -T1 /2 width=1/ -HL12 #TT2 #HTT12 #HTT2
   elim (lift_total VV2 0 1) #VV #H2VV
-  lapply (tpss_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 … H2VV) -V2 /2 width=1/ #HVV
+  lapply (tpss_lift_ge … HVV2 (L2. ⓓWW2) … HV2 … H2VV) -V2 /2 width=1/ #HVV
   @ex2_1_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
 | #V1 #TT1 #T1 #T2 #HTT1 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_bind1 … H) -H #V2 #TT2 #HV12 #HTT12 #H destruct
@@ -76,10 +76,10 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ➡ T2 →
 qed.
 
 lemma tpr_tps_bind: ∀I,V1,V2,T1,T2,U1. V1 ➡ V2 → T1 ➡ T2 →
-                    ⋆. 𝕓{I} V1 ⊢ T1 [0, 1] ▶ U1 →
-                    ∃∃U2. U1 ➡ U2 & ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ▶ U2.
+                    ⋆. ⓑ{I} V1 ⊢ T1 [0, 1] ▶ U1 →
+                    ∃∃U2. U1 ➡ U2 & ⋆. ⓑ{I} V2 ⊢ T2 [0, 1] ▶ U2.
 #I #V1 #V2 #T1 #T2 #U1 #HV12 #HT12 #HTU1
-elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. 𝕓{I} V2) ?) -T1 /2 width=1/ /3 width=3/
+elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. ⓑ{I} V2) ?) -T1 /2 width=1/ /3 width=3/
 qed.
 
 lemma tpr_tpss_ltpr: ∀L1,L2. L1 ➡ L2 → ∀T1,T2. T1 ➡ T2 →
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma
index 24b9e43f5..67fcf4b67 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/reducibility/trf.ma
@@ -18,13 +18,13 @@ include "Basic_2/grammar/term_simple.ma".
 
 (* reducible terms *)
 inductive trf: predicate term ≝
-| trf_abst_sn: ∀V,T.   trf V → trf (𝕔{Abst} V. T)
-| trf_abst_dx: ∀V,T.   trf T → trf (𝕔{Abst} V. T)
-| trf_appl_sn: ∀V,T.   trf V → trf (𝕔{Appl} V. T)
-| trf_appl_dx: ∀V,T.   trf T → trf (𝕔{Appl} V. T)
-| trf_abbr   : ∀V,T.           trf (𝕔{Abbr} V. T)
-| trf_cast   : ∀V,T.           trf (𝕔{Cast} V. T)
-| trf_beta   : ∀V,W,T. trf (𝕔{Appl} V. 𝕔{Abst} W. T)
+| trf_abst_sn: ∀V,T.   trf V → trf (ⓛV. T)
+| trf_abst_dx: ∀V,T.   trf T → trf (ⓛV. T)
+| trf_appl_sn: ∀V,T.   trf V → trf (ⓐV. T)
+| trf_appl_dx: ∀V,T.   trf T → trf (ⓐV. T)
+| trf_abbr   : ∀V,T.           trf (ⓓV. T)
+| trf_cast   : ∀V,T.           trf (ⓣV. T)
+| trf_beta   : ∀V,W,T. trf (ⓐV. ⓛW. T)
 .
 
 interpretation
@@ -40,7 +40,7 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-fact trf_inv_atom_aux: ∀I,T. ℝ[T] → T =  𝕒{I} → False.
+fact trf_inv_atom_aux: ∀I,T. ℝ[T] → T =  ⓪{I} → False.
 #I #T * -T
 [ #V #T #_ #H destruct
 | #V #T #_ #H destruct
@@ -52,10 +52,10 @@ fact trf_inv_atom_aux: ∀I,T. ℝ[T] → T =  𝕒{I} → False.
 ]
 qed.
 
-lemma trf_inv_atom: ∀I. ℝ[𝕒{I}] → False.
+lemma trf_inv_atom: ∀I. ℝ[⓪{I}] → False.
 /2 width=4/ qed-.
 
-fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T =  𝕔{Abst} W. U → ℝ[W] ∨ ℝ[U].
+fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T =  ⓛW. U → ℝ[W] ∨ ℝ[U].
 #W #U #T * -T
 [ #V #T #HV #H destruct /2 width=1/
 | #V #T #HT #H destruct /2 width=1/
@@ -67,10 +67,10 @@ fact trf_inv_abst_aux: ∀W,U,T. ℝ[T] → T =  𝕔{Abst} W. U → ℝ[W] ∨
 ]
 qed.
 
-lemma trf_inv_abst: ∀V,T. ℝ[𝕔{Abst}V.T] → ℝ[V] ∨ ℝ[T].
+lemma trf_inv_abst: ∀V,T. ℝ[ⓛV.T] → ℝ[V] ∨ ℝ[T].
 /2 width=3/ qed-.
 
-fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T =  𝕔{Appl} W. U →
+fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T =  ⓐW. U →
                        ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
 #W #U #T * -T
 [ #V #T #_ #H destruct
@@ -84,35 +84,35 @@ fact trf_inv_appl_aux: ∀W,U,T. ℝ[T] → T =  𝕔{Appl} W. U →
 ]
 qed.
 
-lemma trf_inv_appl: ∀W,U. ℝ[𝕔{Appl}W.U] → ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
+lemma trf_inv_appl: ∀W,U. ℝ[ⓐW.U] → ∨∨ ℝ[W] | ℝ[U] | (𝕊[U] → False).
 /2 width=3/ qed-.
 
-lemma tif_inv_abbr: ∀V,T. 𝕀[𝕔{Abbr}V.T] → False.
+lemma tif_inv_abbr: ∀V,T. 𝕀[ⓓV.T] → False.
 /2 width=1/ qed-.
 
-lemma tif_inv_abst: ∀V,T. 𝕀[𝕔{Abst}V.T] → 𝕀[V] ∧ 𝕀[T].
+lemma tif_inv_abst: ∀V,T. 𝕀[ⓛV.T] → 𝕀[V] ∧ 𝕀[T].
 /4 width=1/ qed-.
 
-lemma tif_inv_appl: ∀V,T. 𝕀[𝕔{Appl}V.T] → ∧∧ 𝕀[V] & 𝕀[T] & 𝕊[T].
+lemma tif_inv_appl: ∀V,T. 𝕀[ⓐV.T] → ∧∧ 𝕀[V] & 𝕀[T] & 𝕊[T].
 #V #T #HVT @and3_intro /3 width=1/
 generalize in match HVT; -HVT elim T -T //
 * // * #U #T #_ #_ #H elim (H ?) -H /2 width=1/
 qed-.
 
-lemma tif_inv_cast: ∀V,T. 𝕀[𝕔{Cast}V.T] → False.
+lemma tif_inv_cast: ∀V,T. 𝕀[ⓣV.T] → False.
 /2 width=1/ qed-.
 
 (* Basic properties *********************************************************)
 
-lemma tif_atom: ∀I. 𝕀[𝕒{I}].
+lemma tif_atom: ∀I. 𝕀[⓪{I}].
 /2 width=4/ qed.
 
-lemma tif_abst: ∀V,T. 𝕀[V] →  𝕀[T] →  𝕀[𝕔 {Abst}V.T].
+lemma tif_abst: ∀V,T. 𝕀[V] →  𝕀[T] →  𝕀[ⓛV.T].
 #V #T #HV #HT #H
 elim (trf_inv_abst … H) -H /2 width=1/
 qed.
 
-lemma tif_appl: ∀V,T. 𝕀[V] →  𝕀[T] →  𝕊[T] → 𝕀[𝕔{Appl}V.T].
+lemma tif_appl: ∀V,T. 𝕀[V] →  𝕀[T] →  𝕊[T] → 𝕀[ⓐV.T].
 #V #T #HV #HT #S #H
 elim (trf_inv_appl … H) -H /2 width=1/
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/aaa.ma b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa.ma
index ea3e2d1c7..ecf6b6833 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/static/aaa.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/static/aaa.ma
@@ -18,16 +18,111 @@ include "Basic_2/substitution/ldrop.ma".
 (* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
 
 inductive aaa: lenv → term → predicate aarity ≝
-| aaa_sort: ∀L,k. aaa L (⋆k) 𝕒
-| aaa_lref: ∀I,L,K,V,B,i. ⇩[0, i] L ≡ K. 𝕓{I} V → aaa K V B → aaa L (#i) B
+| aaa_sort: ∀L,k. aaa L (⋆k) ⓪
+| aaa_lref: ∀I,L,K,V,B,i. ⇩[0, i] L ≡ K. ⓑ{I} V → aaa K V B → aaa L (#i) B
 | aaa_abbr: ∀L,V,T,B,A.
-            aaa L V B → aaa (L. 𝕓{Abbr} V) T A → aaa L (𝕔{Abbr} V. T) A
+            aaa L V B → aaa (L. ⓓV) T A → aaa L (ⓓV. T) A
 | aaa_abst: ∀L,V,T,B,A.
-            aaa L V B → aaa (L. 𝕓{Abst} V) T A → aaa L (𝕔{Abst} V. T) (𝕔 B. A)
-| aaa_appl: ∀L,V,T,B,A. aaa L V B → aaa L T (𝕔 B. A) → aaa L (𝕔{Appl} V. T) A
-| aaa_cast: ∀L,V,T,A. aaa L V A → aaa L T A → aaa L (𝕔{Cast} V. T) A
+            aaa L V B → aaa (L. ⓛV) T A → aaa L (ⓛV. T) (②B. A)
+| aaa_appl: ∀L,V,T,B,A. aaa L V B → aaa L T (②B. A) → aaa L (ⓐV. T) A
+| aaa_cast: ∀L,V,T,A. aaa L V A → aaa L T A → aaa L (ⓣV. T) A
 .
 
-interpretation
-   "atomic arity assignment (term)"
+interpretation "atomic arity assignment (term)"
    'AtomicArity L T A = (aaa L T A).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact aaa_inv_sort_aux: ∀L,T,A. L ⊢ T ÷ A → ∀k. T = ⋆k → A = ⓪.
+#L #T #A * -L -T -A
+[ //
+| #I #L #K #V #B #i #_ #_ #k #H destruct
+| #L #V #T #B #A #_ #_ #k #H destruct
+| #L #V #T #B #A #_ #_ #k #H destruct
+| #L #V #T #B #A #_ #_ #k #H destruct
+| #L #V #T #A #_ #_ #k #H destruct
+]
+qed.
+
+lemma aaa_inv_sort: ∀L,A,k. L ⊢ ⋆k ÷ A → A = ⓪.
+/2 width=5/ qed-.
+
+fact aaa_inv_lref_aux: ∀L,T,A. L ⊢ T ÷ A → ∀i. T = #i →
+                       ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ÷ A.
+#L #T #A * -L -T -A
+[ #L #k #i #H destruct
+| #I #L #K #V #B #j #HLK #HB #i #H destruct /2 width=5/
+| #L #V #T #B #A #_ #_ #i #H destruct
+| #L #V #T #B #A #_ #_ #i #H destruct
+| #L #V #T #B #A #_ #_ #i #H destruct
+| #L #V #T #A #_ #_ #i #H destruct
+]
+qed.
+
+lemma aaa_inv_lref: ∀L,A,i. L ⊢ #i ÷ A →
+                    ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ÷ A.
+/2 width=3/ qed-.
+
+fact aaa_inv_abbr_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓓW. U →
+                       ∃∃B. L ⊢ W ÷ B & L. ⓓW ⊢ U ÷ A.
+#L #T #A * -L -T -A
+[ #L #k #W #U #H destruct
+| #I #L #K #V #B #i #_ #_ #W #U #H destruct
+| #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=2/
+| #L #V #T #B #A #_ #_ #W #U #H destruct
+| #L #V #T #B #A #_ #_ #W #U #H destruct
+| #L #V #T #A #_ #_ #W #U #H destruct
+]
+qed.
+
+lemma aaa_inv_abbr: ∀L,V,T,A. L ⊢ ⓓV. T ÷ A →
+                    ∃∃B. L ⊢ V ÷ B & L. ⓓV ⊢ T ÷ A.
+/2 width=3/ qed-.
+
+fact aaa_inv_abst_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓛW. U →
+                       ∃∃B1,B2. L ⊢ W ÷ B1 & L. ⓛW ⊢ U ÷ B2 & A = ②B1. B2.
+#L #T #A * -L -T -A
+[ #L #k #W #U #H destruct
+| #I #L #K #V #B #i #_ #_ #W #U #H destruct
+| #L #V #T #B #A #_ #_ #W #U #H destruct
+| #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=5/
+| #L #V #T #B #A #_ #_ #W #U #H destruct
+| #L #V #T #A #_ #_ #W #U #H destruct
+]
+qed.
+
+lemma aaa_inv_abst: ∀L,W,T,A. L ⊢ ⓛW. T ÷ A →
+                    ∃∃B1,B2. L ⊢ W ÷ B1 & L. ⓛW ⊢ T ÷ B2 & A = ②B1. B2.
+/2 width=3/ qed-.
+
+fact aaa_inv_appl_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓐW. U →
+                       ∃∃B. L ⊢ W ÷ B & L ⊢ U ÷ ②B. A.
+#L #T #A * -L -T -A
+[ #L #k #W #U #H destruct
+| #I #L #K #V #B #i #_ #_ #W #U #H destruct
+| #L #V #T #B #A #_ #_ #W #U #H destruct
+| #L #V #T #B #A #_ #_ #W #U #H destruct
+| #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=3/
+| #L #V #T #A #_ #_ #W #U #H destruct
+]
+qed.
+
+lemma aaa_inv_appl: ∀L,V,T,A. L ⊢ ⓐV. T ÷ A →
+                    ∃∃B. L ⊢ V ÷ B & L ⊢ T ÷ ②B. A.
+/2 width=3/ qed-.
+
+fact aaa_inv_cast_aux: ∀L,T,A. L ⊢ T ÷ A → ∀W,U. T = ⓣW. U →
+                       L ⊢ W ÷ A ∧ L ⊢ U ÷ A.
+#L #T #A * -L -T -A
+[ #L #k #W #U #H destruct
+| #I #L #K #V #B #i #_ #_ #W #U #H destruct
+| #L #V #T #B #A #_ #_ #W #U #H destruct
+| #L #V #T #B #A #_ #_ #W #U #H destruct
+| #L #V #T #B #A #_ #_ #W #U #H destruct
+| #L #V #T #A #HV #HT #W #U #H destruct /2 width=1/
+]
+qed.
+
+lemma aaa_inv_cast: ∀L,W,T,A. L ⊢ ⓣW. T ÷ A →
+                    L ⊢ W ÷ A ∧ L ⊢ T ÷ A.
+/2 width=3/ qed-.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba.ma b/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba.ma
index 37f5bf73a..d6750c3d5 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/static/lsuba.ma
@@ -18,9 +18,9 @@ include "Basic_2/static/aaa.ma".
 
 inductive lsuba: relation lenv ≝
 | lsuba_atom: lsuba (⋆) (⋆)
-| lsuba_pair: ∀I,L1,L2,V. lsuba L1 L2 → lsuba (L1. 𝕓{I} V) (L2. 𝕓{I} V)
+| lsuba_pair: ∀I,L1,L2,V. lsuba L1 L2 → lsuba (L1. ⓑ{I} V) (L2. ⓑ{I} V)
 | lsuba_abbr: ∀L1,L2,V,W,A. L1 ⊢ V ÷ A → L2 ⊢ W ÷ A → 
-              lsuba L1 L2 → lsuba (L1. 𝕓{Abbr} V) (L2. 𝕓{Abst} W)
+              lsuba L1 L2 → lsuba (L1. ⓓV) (L2. ⓛW)
 .
 
 interpretation
@@ -29,10 +29,10 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-fact lsuba_inv_pair2_aux: ∀L1,L2. L1 ÷⊑ L2 → ∀I,K2,W. L2 = K2. 𝕓{I} W →
-                          (∃∃K1. K1 ÷⊑ K2 & L1 = K1. 𝕓{I} W) ∨
+fact lsuba_inv_pair2_aux: ∀L1,L2. L1 ÷⊑ L2 → ∀I,K2,W. L2 = K2. ⓑ{I} W →
+                          (∃∃K1. K1 ÷⊑ K2 & L1 = K1. ⓑ{I} W) ∨
                           ∃∃K1,V,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 &
-                                    L1 = K1. 𝕓{Abbr} V & I = Abst.
+                                    L1 = K1. ⓓV & I = Abst.
 #L1 #L2 * -L1 -L2
 [ #I #K2 #W #H destruct
 | #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
@@ -40,10 +40,10 @@ fact lsuba_inv_pair2_aux: ∀L1,L2. L1 ÷⊑ L2 → ∀I,K2,W. L2 = K2. 𝕓{I}
 ]
 qed.
 
-lemma lsuba_inv_pair2: ∀I,L1,K2,W. L1 ÷⊑ K2. 𝕓{I} W →
-                       (∃∃K1. K1 ÷⊑ K2 & L1 = K1. 𝕓{I} W) ∨
+lemma lsuba_inv_pair2: ∀I,L1,K2,W. L1 ÷⊑ K2. ⓑ{I} W →
+                       (∃∃K1. K1 ÷⊑ K2 & L1 = K1. ⓑ{I} W) ∨
                        ∃∃K1,V,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 &
-                                 L1 = K1. 𝕓{Abbr} V & I = Abst.
+                                 L1 = K1. ⓓV & I = Abst.
 /2 width=3/ qed-.
 
 (* Basic properties *********************************************************)
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma
index 869b47757..eb4bd4865 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma
@@ -19,7 +19,7 @@ include "Basic_2/grammar/genv.ma".
 inductive gdrop (e:nat): relation genv ≝
 | gdrop_gt: ∀G. |G| ≤ e → gdrop e G (⋆)
 | gdrop_eq: ∀G. |G| = e + 1 → gdrop e G G
-| gdrop_lt: ∀I,G1,G2,V. e < |G1| → gdrop e G1 G2 → gdrop e (G1. 𝕓{I} V) G2
+| gdrop_lt: ∀I,G1,G2,V. e < |G1| → gdrop e G1 G2 → gdrop e (G1. ⓑ{I} V) G2
 .
 
 interpretation "global slicing" 
@@ -50,7 +50,7 @@ lemma gdrop_inv_eq: ∀G1,G2,e. ⇩[e] G1 ≡ G2 → |G1| = e + 1 → G1 = G2.
 ]
 qed-.
 
-fact gdrop_inv_lt_aux: ∀I,G,G1,G2,V,e. ⇩[e] G ≡ G2 → G = G1. 𝕓{I} V →
+fact gdrop_inv_lt_aux: ∀I,G,G1,G2,V,e. ⇩[e] G ≡ G2 → G = G1. ⓑ{I} V →
                        e < |G1| → ⇩[e] G1 ≡ G2.
 #I #G #G1 #G2 #V #e * -G -G2
 [ #G #H1 #H destruct #H2
@@ -64,7 +64,7 @@ fact gdrop_inv_lt_aux: ∀I,G,G1,G2,V,e. ⇩[e] G ≡ G2 → G = G1. 𝕓{I} V 
 qed.
 
 lemma gdrop_inv_lt: ∀I,G1,G2,V,e.
-                    ⇩[e] G1. 𝕓{I} V ≡ G2 → e < |G1| → ⇩[e] G1 ≡ G2.
+                    ⇩[e] G1. ⓑ{I} V ≡ G2 → e < |G1| → ⇩[e] G1 ≡ G2.
 /2 width=5/ qed-.
 
 (* Basic properties *********************************************************)
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
index d3788f410..c7fc055e7 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop.ma
@@ -21,11 +21,11 @@ include "Basic_2/substitution/lift.ma".
 (* Basic_1: includes: ldrop_skip_bind *)
 inductive ldrop: nat → nat → relation lenv ≝
 | ldrop_atom : ∀d,e. ldrop d e (⋆) (⋆)
-| ldrop_pair : ∀L,I,V. ldrop 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V)
-| ldrop_ldrop: ∀L1,L2,I,V,e. ldrop 0 e L1 L2 → ldrop 0 (e + 1) (L1. 𝕓{I} V) L2
+| ldrop_pair : ∀L,I,V. ldrop 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V)
+| ldrop_ldrop: ∀L1,L2,I,V,e. ldrop 0 e L1 L2 → ldrop 0 (e + 1) (L1. ⓑ{I} V) L2
 | ldrop_skip : ∀L1,L2,I,V1,V2,d,e.
                ldrop d e L1 L2 → ⇧[d,e] V2 ≡ V1 →
-               ldrop (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2)
+               ldrop (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
 .
 
 interpretation "local slicing" 'RDrop d e L1 L2 = (ldrop d e L1 L2).
@@ -60,8 +60,8 @@ lemma ldrop_inv_atom1: ∀d,e,L2. ⇩[d, e] ⋆ ≡ L2 → L2 = ⋆.
 /2 width=5/ qed-.
 
 fact ldrop_inv_O1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → d = 0 →
-                       ∀K,I,V. L1 = K. 𝕓{I} V → 
-                       (e = 0 ∧ L2 = K. 𝕓{I} V) ∨
+                       ∀K,I,V. L1 = K. ⓑ{I} V → 
+                       (e = 0 ∧ L2 = K. ⓑ{I} V) ∨
                        (0 < e ∧ ⇩[d, e - 1] K ≡ L2).
 #d #e #L1 #L2 * -d -e -L1 -L2
 [ #d #e #_ #K #I #V #H destruct
@@ -71,24 +71,24 @@ fact ldrop_inv_O1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → d = 0 →
 ]
 qed.
 
-lemma ldrop_inv_O1: ∀e,K,I,V,L2. ⇩[0, e] K. 𝕓{I} V ≡ L2 →
-                    (e = 0 ∧ L2 = K. 𝕓{I} V) ∨
+lemma ldrop_inv_O1: ∀e,K,I,V,L2. ⇩[0, e] K. ⓑ{I} V ≡ L2 →
+                    (e = 0 ∧ L2 = K. ⓑ{I} V) ∨
                     (0 < e ∧ ⇩[0, e - 1] K ≡ L2).
 /2 width=3/ qed-.
 
 (* Basic_1: was: ldrop_gen_ldrop *)
 lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2.
-                        ⇩[0, e] K. 𝕓{I} V ≡ L2 → 0 < e → ⇩[0, e - 1] K ≡ L2.
+                        ⇩[0, e] K. ⓑ{I} V ≡ L2 → 0 < e → ⇩[0, e - 1] K ≡ L2.
 #e #K #I #V #L2 #H #He
 elim (ldrop_inv_O1 … H) -H * // #H destruct
 elim (lt_refl_false … He)
 qed-.
 
 fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d →
-                          ∀I,K1,V1. L1 = K1. 𝕓{I} V1 →
+                          ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
                           ∃∃K2,V2. ⇩[d - 1, e] K1 ≡ K2 &
                                    ⇧[d - 1, e] V2 ≡ V1 & 
-                                   L2 = K2. 𝕓{I} V2.
+                                   L2 = K2. ⓑ{I} V2.
 #d #e #L1 #L2 * -d -e -L1 -L2
 [ #d #e #_ #I #K #V #H destruct
 | #L #I #V #H elim (lt_refl_false … H)
@@ -98,17 +98,17 @@ fact ldrop_inv_skip1_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d →
 qed.
 
 (* Basic_1: was: ldrop_gen_skip_l *)
-lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ⇩[d, e] K1. 𝕓{I} V1 ≡ L2 → 0 < d →
+lemma ldrop_inv_skip1: ∀d,e,I,K1,V1,L2. ⇩[d, e] K1. ⓑ{I} V1 ≡ L2 → 0 < d →
                        ∃∃K2,V2. ⇩[d - 1, e] K1 ≡ K2 &
                                 ⇧[d - 1, e] V2 ≡ V1 & 
-                                L2 = K2. 𝕓{I} V2.
+                                L2 = K2. ⓑ{I} V2.
 /2 width=3/ qed-.
 
 fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d →
-                          ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
+                          ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
                           ∃∃K1,V1. ⇩[d - 1, e] K1 ≡ K2 &
                                    ⇧[d - 1, e] V2 ≡ V1 & 
-                                   L1 = K1. 𝕓{I} V1.
+                                   L1 = K1. ⓑ{I} V1.
 #d #e #L1 #L2 * -d -e -L1 -L2
 [ #d #e #_ #I #K #V #H destruct
 | #L #I #V #H elim (lt_refl_false … H)
@@ -118,9 +118,9 @@ fact ldrop_inv_skip2_aux: ∀d,e,L1,L2. ⇩[d, e] L1 ≡ L2 → 0 < d →
 qed.
 
 (* Basic_1: was: ldrop_gen_skip_r *)
-lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ⇩[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d →
+lemma ldrop_inv_skip2: ∀d,e,I,L1,K2,V2. ⇩[d, e] L1 ≡ K2. ⓑ{I} V2 → 0 < d →
                        ∃∃K1,V1. ⇩[d - 1, e] K1 ≡ K2 & ⇧[d - 1, e] V2 ≡ V1 &
-                                L1 = K1. 𝕓{I} V1.
+                                L1 = K1. ⓑ{I} V1.
 /2 width=3/ qed-.
 
 (* Basic properties *********************************************************)
@@ -131,15 +131,15 @@ lemma ldrop_refl: ∀L. ⇩[0, 0] L ≡ L.
 qed.
 
 lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e.
-                      ⇩[0, e - 1] L1 ≡ L2 → 0 < e → ⇩[0, e] L1. 𝕓{I} V ≡ L2.
+                      ⇩[0, e - 1] L1 ≡ L2 → 0 < e → ⇩[0, e] L1. ⓑ{I} V ≡ L2.
 #L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
 qed.
 
 lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
-                               ∀K1,V,i. ⇩[0, i] L1 ≡ K1. 𝕓{Abbr} V →
+                               ∀K1,V,i. ⇩[0, i] L1 ≡ K1. ⓓV →
                                d ≤ i → i < d + e →
                                ∃∃K2. K1 [0, d + e - i - 1] ≼ K2 &
-                                     ⇩[0, i] L2 ≡ K2. 𝕓{Abbr} V.
+                                     ⇩[0, i] L2 ≡ K2. ⓓV.
 #L1 #L2 #d #e #H elim H -L1 -L2 -d -e
 [ #d #e #K1 #V #i #H
   lapply (ldrop_inv_atom1 … H) -H #H destruct
@@ -167,7 +167,7 @@ qed.
 (* Basic forvard lemmas *****************************************************)
 
 (* Basic_1: was: ldrop_S *)
-lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇩[O, e] L1 ≡ K2. 𝕓{I2} V2 →
+lemma ldrop_fwd_ldrop2: ∀L1,I2,K2,V2,e. ⇩[O, e] L1 ≡ K2. ⓑ{I2} V2 →
                         ⇩[O, e + 1] L1 ≡ K2.
 #L1 elim L1 -L1
 [ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct
@@ -188,7 +188,7 @@ lemma ldrop_fwd_lw: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 → #[L2] ≤ #[L1].
 qed-. 
 
 lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e.
-                               ⇩[0, e] L1 ≡ K2. 𝕓{I2} V2 → e < |L1|.
+                               ⇩[0, e] L1 ≡ K2. ⓑ{I2} V2 → e < |L1|.
 #L1 elim L1 -L1
 [ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct
 | #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma
index 2c4b8879f..91c0c6b70 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ldrop_ldrop.ma
@@ -57,9 +57,9 @@ qed.
 
 (* Basic_1: was: ldrop_conf_lt *)
 theorem ldrop_conf_lt: ∀d1,e1,L,L1. ⇩[d1, e1] L ≡ L1 →
-                       ∀e2,K2,I,V2. ⇩[0, e2] L ≡ K2. 𝕓{I} V2 →
+                       ∀e2,K2,I,V2. ⇩[0, e2] L ≡ K2. ⓑ{I} V2 →
                        e2 < d1 → let d ≝ d1 - e2 - 1 in
-                       ∃∃K1,V1. ⇩[0, e2] L1 ≡ K1. 𝕓{I} V1 &
+                       ∃∃K1,V1. ⇩[0, e2] L1 ≡ K1. ⓑ{I} V1 &
                                 ⇩[d, e1] K2 ≡ K1 & ⇧[d, e1] V1 ≡ V2.
 #d1 #e1 #L #L1 #H elim H -d1 -e1 -L -L1
 [ #d #e #e2 #K2 #I #V2 #H
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma
index b588b29b7..f9d1ddb93 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma
@@ -27,10 +27,10 @@ inductive lift: nat → nat → relation term ≝
 | lift_gref   : ∀p,d,e. lift d e (§p) (§p)
 | lift_bind   : ∀I,V1,V2,T1,T2,d,e.
                 lift d e V1 V2 → lift (d + 1) e T1 T2 →
-                lift d e (𝕓{I} V1. T1) (𝕓{I} V2. T2)
+                lift d e (ⓑ{I} V1. T1) (ⓑ{I} V2. T2)
 | lift_flat   : ∀I,V1,V2,T1,T2,d,e.
                 lift d e V1 V2 → lift d e T1 T2 →
-                lift d e (𝕗{I} V1. T1) (𝕗{I} V2. T2)
+                lift d e (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
 .
 
 interpretation "relocation" 'RLift d e T1 T2 = (lift d e T1 T2).
@@ -95,9 +95,9 @@ lemma lift_inv_gref1: ∀d,e,T2,p. ⇧[d,e] §p ≡ T2 → T2 = §p.
 /2 width=5/ qed-.
 
 fact lift_inv_bind1_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 →
-                         ∀I,V1,U1. T1 = 𝕓{I} V1.U1 →
+                         ∀I,V1,U1. T1 = ⓑ{I} V1.U1 →
                          ∃∃V2,U2. ⇧[d,e] V1 ≡ V2 & ⇧[d+1,e] U1 ≡ U2 &
-                                  T2 = 𝕓{I} V2. U2.
+                                  T2 = ⓑ{I} V2. U2.
 #d #e #T1 #T2 * -d -e -T1 -T2
 [ #k #d #e #I #V1 #U1 #H destruct
 | #i #d #e #_ #I #V1 #U1 #H destruct
@@ -108,15 +108,15 @@ fact lift_inv_bind1_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 →
 ]
 qed.
 
-lemma lift_inv_bind1: ∀d,e,T2,I,V1,U1. ⇧[d,e] 𝕓{I} V1. U1 ≡ T2 →
+lemma lift_inv_bind1: ∀d,e,T2,I,V1,U1. ⇧[d,e] ⓑ{I} V1. U1 ≡ T2 →
                       ∃∃V2,U2. ⇧[d,e] V1 ≡ V2 & ⇧[d+1,e] U1 ≡ U2 &
-                               T2 = 𝕓{I} V2. U2.
+                               T2 = ⓑ{I} V2. U2.
 /2 width=3/ qed-.
 
 fact lift_inv_flat1_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 →
-                         ∀I,V1,U1. T1 = 𝕗{I} V1.U1 →
+                         ∀I,V1,U1. T1 = ⓕ{I} V1.U1 →
                          ∃∃V2,U2. ⇧[d,e] V1 ≡ V2 & ⇧[d,e] U1 ≡ U2 &
-                                  T2 = 𝕗{I} V2. U2.
+                                  T2 = ⓕ{I} V2. U2.
 #d #e #T1 #T2 * -d -e -T1 -T2
 [ #k #d #e #I #V1 #U1 #H destruct
 | #i #d #e #_ #I #V1 #U1 #H destruct
@@ -127,9 +127,9 @@ fact lift_inv_flat1_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 →
 ]
 qed.
 
-lemma lift_inv_flat1: ∀d,e,T2,I,V1,U1. ⇧[d,e] 𝕗{I} V1. U1 ≡ T2 →
+lemma lift_inv_flat1: ∀d,e,T2,I,V1,U1. ⇧[d,e] ⓕ{I} V1. U1 ≡ T2 →
                       ∃∃V2,U2. ⇧[d,e] V1 ≡ V2 & ⇧[d,e] U1 ≡ U2 &
-                               T2 = 𝕗{I} V2. U2.
+                               T2 = ⓕ{I} V2. U2.
 /2 width=3/ qed-.
 
 fact lift_inv_sort2_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k.
@@ -198,9 +198,9 @@ lemma lift_inv_gref2: ∀d,e,T1,p. ⇧[d,e] T1 ≡ §p → T1 = §p.
 /2 width=5/ qed-.
 
 fact lift_inv_bind2_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 →
-                         ∀I,V2,U2. T2 = 𝕓{I} V2.U2 →
+                         ∀I,V2,U2. T2 = ⓑ{I} V2.U2 →
                          ∃∃V1,U1. ⇧[d,e] V1 ≡ V2 & ⇧[d+1,e] U1 ≡ U2 &
-                                  T1 = 𝕓{I} V1. U1.
+                                  T1 = ⓑ{I} V1. U1.
 #d #e #T1 #T2 * -d -e -T1 -T2
 [ #k #d #e #I #V2 #U2 #H destruct
 | #i #d #e #_ #I #V2 #U2 #H destruct
@@ -212,15 +212,15 @@ fact lift_inv_bind2_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 →
 qed.
 
 (* Basic_1: was: lift_gen_bind *)
-lemma lift_inv_bind2: ∀d,e,T1,I,V2,U2. ⇧[d,e] T1 ≡  𝕓{I} V2. U2 →
+lemma lift_inv_bind2: ∀d,e,T1,I,V2,U2. ⇧[d,e] T1 ≡  ⓑ{I} V2. U2 →
                       ∃∃V1,U1. ⇧[d,e] V1 ≡ V2 & ⇧[d+1,e] U1 ≡ U2 &
-                               T1 = 𝕓{I} V1. U1.
+                               T1 = ⓑ{I} V1. U1.
 /2 width=3/ qed-.
 
 fact lift_inv_flat2_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 →
-                         ∀I,V2,U2. T2 = 𝕗{I} V2.U2 →
+                         ∀I,V2,U2. T2 = ⓕ{I} V2.U2 →
                          ∃∃V1,U1. ⇧[d,e] V1 ≡ V2 & ⇧[d,e] U1 ≡ U2 &
-                                  T1 = 𝕗{I} V1. U1.
+                                  T1 = ⓕ{I} V1. U1.
 #d #e #T1 #T2 * -d -e -T1 -T2
 [ #k #d #e #I #V2 #U2 #H destruct
 | #i #d #e #_ #I #V2 #U2 #H destruct
@@ -232,12 +232,12 @@ fact lift_inv_flat2_aux: ∀d,e,T1,T2. ⇧[d,e] T1 ≡ T2 →
 qed.
 
 (* Basic_1: was: lift_gen_flat *)
-lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ⇧[d,e] T1 ≡  𝕗{I} V2. U2 →
+lemma lift_inv_flat2: ∀d,e,T1,I,V2,U2. ⇧[d,e] T1 ≡  ⓕ{I} V2. U2 →
                       ∃∃V1,U1. ⇧[d,e] V1 ≡ V2 & ⇧[d,e] U1 ≡ U2 &
-                               T1 = 𝕗{I} V1. U1.
+                               T1 = ⓕ{I} V1. U1.
 /2 width=3/ qed-.
 
-lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇧[d, e] 𝕔{I} V. T ≡ V → False.
+lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇧[d, e] ②{I} V. T ≡ V → False.
 #d #e #J #V elim V -V
 [ * #i #T #H
   [ lapply (lift_inv_sort2 … H) -H #H destruct
@@ -251,7 +251,7 @@ lemma lift_inv_pair_xy_x: ∀d,e,I,V,T. ⇧[d, e] 𝕔{I} V. T ≡ V → False.
 ]
 qed-.
 
-lemma lift_inv_pair_xy_y: ∀I,T,V,d,e. ⇧[d, e] 𝕔{I} V. T ≡ T → False.
+lemma lift_inv_pair_xy_y: ∀I,T,V,d,e. ⇧[d, e] ②{I} V. T ≡ T → False.
 #J #T elim T -T
 [ * #i #V #d #e #H
   [ lapply (lift_inv_sort2 … H) -H #H destruct
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma
index 9adf78710..9f5547ed0 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps.ma
@@ -19,13 +19,13 @@ include "Basic_2/substitution/tps.ma".
 (* Basic_1: includes: csubst1_bind *)
 inductive ltps: nat → nat → relation lenv ≝
 | ltps_atom: ∀d,e. ltps d e (⋆) (⋆)
-| ltps_pair: ∀L,I,V. ltps 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V)
+| ltps_pair: ∀L,I,V. ltps 0 0 (L. ⓑ{I} V) (L. ⓑ{I} V)
 | ltps_tps2: ∀L1,L2,I,V1,V2,e.
              ltps 0 e L1 L2 → L2 ⊢ V1 [0, e] ▶ V2 →
-             ltps 0 (e + 1) (L1. 𝕓{I} V1) L2. 𝕓{I} V2
+             ltps 0 (e + 1) (L1. ⓑ{I} V1) L2. ⓑ{I} V2
 | ltps_tps1: ∀L1,L2,I,V1,V2,d,e.
              ltps d e L1 L2 → L2 ⊢ V1 [d, e] ▶ V2 →
-             ltps (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2)
+             ltps (d + 1) e (L1. ⓑ{I} V1) (L2. ⓑ{I} V2)
 .
 
 interpretation "parallel substritution (local environment)"
@@ -35,14 +35,14 @@ interpretation "parallel substritution (local environment)"
 
 lemma ltps_tps2_lt: ∀L1,L2,I,V1,V2,e.
                     L1 [0, e - 1] ▶ L2 → L2 ⊢ V1 [0, e - 1] ▶ V2 →
-                    0 < e → L1. 𝕓{I} V1 [0, e] ▶ L2. 𝕓{I} V2.
+                    0 < e → L1. ⓑ{I} V1 [0, e] ▶ L2. ⓑ{I} V2.
 #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
 >(plus_minus_m_m e 1) /2 width=1/
 qed.
 
 lemma ltps_tps1_lt: ∀L1,L2,I,V1,V2,d,e.
                     L1 [d - 1, e] ▶ L2 → L2 ⊢ V1 [d - 1, e] ▶ V2 →
-                    0 < d → L1. 𝕓{I} V1 [d, e] ▶ L2. 𝕓{I} V2.
+                    0 < d → L1. ⓑ{I} V1 [d, e] ▶ L2. ⓑ{I} V2.
 #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
 >(plus_minus_m_m d 1) /2 width=1/
 qed.
@@ -80,10 +80,10 @@ lemma ltps_inv_atom1: ∀d,e,L2. ⋆ [d, e] ▶ L2 → L2 = ⋆.
 /2 width=5/ qed-.
 
 fact ltps_inv_tps21_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → d = 0 → 0 < e →
-                         ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
+                         ∀K1,I,V1. L1 = K1. ⓑ{I} V1 →
                          ∃∃K2,V2. K1 [0, e - 1] ▶ K2 &
                                   K2 ⊢ V1 [0, e - 1] ▶ V2 &
-                                  L2 = K2. 𝕓{I} V2.
+                                  L2 = K2. ⓑ{I} V2.
 #d #e #L1 #L2 * -d -e -L1 -L2
 [ #d #e #_ #_ #K1 #I #V1 #H destruct
 | #L1 #I #V #_ #H elim (lt_refl_false … H)
@@ -92,16 +92,16 @@ fact ltps_inv_tps21_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → d = 0 → 0 < e →
 ]
 qed.
 
-lemma ltps_inv_tps21: ∀e,K1,I,V1,L2. K1. 𝕓{I} V1 [0, e] ▶ L2 → 0 < e →
+lemma ltps_inv_tps21: ∀e,K1,I,V1,L2. K1. ⓑ{I} V1 [0, e] ▶ L2 → 0 < e →
                       ∃∃K2,V2. K1 [0, e - 1] ▶ K2 & K2 ⊢ V1 [0, e - 1] ▶ V2 &
-                               L2 = K2. 𝕓{I} V2.
+                               L2 = K2. ⓑ{I} V2.
 /2 width=5/ qed-.
 
 fact ltps_inv_tps11_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → 0 < d →
-                         ∀I,K1,V1. L1 = K1. 𝕓{I} V1 →
+                         ∀I,K1,V1. L1 = K1. ⓑ{I} V1 →
                          ∃∃K2,V2. K1 [d - 1, e] ▶ K2 &
                                   K2 ⊢ V1 [d - 1, e] ▶ V2 &
-                                  L2 = K2. 𝕓{I} V2.
+                                  L2 = K2. ⓑ{I} V2.
 #d #e #L1 #L2 * -d -e -L1 -L2
 [ #d #e #_ #I #K1 #V1 #H destruct
 | #L #I #V #H elim (lt_refl_false … H)
@@ -110,10 +110,10 @@ fact ltps_inv_tps11_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → 0 < d →
 ]
 qed.
 
-lemma ltps_inv_tps11: ∀d,e,I,K1,V1,L2. K1. 𝕓{I} V1 [d, e] ▶ L2 → 0 < d →
+lemma ltps_inv_tps11: ∀d,e,I,K1,V1,L2. K1. ⓑ{I} V1 [d, e] ▶ L2 → 0 < d →
                       ∃∃K2,V2. K1 [d - 1, e] ▶ K2 &
                                   K2 ⊢ V1 [d - 1, e] ▶ V2 &
-                                  L2 = K2. 𝕓{I} V2.
+                                  L2 = K2. ⓑ{I} V2.
 /2 width=3/ qed-.
 
 fact ltps_inv_atom2_aux: ∀d,e,L1,L2.
@@ -130,10 +130,10 @@ lemma ltps_inv_atom2: ∀d,e,L1. L1 [d, e] ▶ ⋆ → L1 = ⋆.
 /2 width=5/ qed-.
 
 fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → d = 0 → 0 < e →
-                         ∀K2,I,V2. L2 = K2. 𝕓{I} V2 →
+                         ∀K2,I,V2. L2 = K2. ⓑ{I} V2 →
                          ∃∃K1,V1. K1 [0, e - 1] ▶ K2 &
                                   K2 ⊢ V1 [0, e - 1] ▶ V2 &
-                                  L1 = K1. 𝕓{I} V1.
+                                  L1 = K1. ⓑ{I} V1.
 #d #e #L1 #L2 * -d -e -L1 -L2
 [ #d #e #_ #_ #K1 #I #V1 #H destruct
 | #L1 #I #V #_ #H elim (lt_refl_false … H)
@@ -142,16 +142,16 @@ fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → d = 0 → 0 < e →
 ]
 qed.
 
-lemma ltps_inv_tps22: ∀e,L1,K2,I,V2. L1 [0, e] ▶ K2. 𝕓{I} V2 → 0 < e →
+lemma ltps_inv_tps22: ∀e,L1,K2,I,V2. L1 [0, e] ▶ K2. ⓑ{I} V2 → 0 < e →
                       ∃∃K1,V1. K1 [0, e - 1] ▶ K2 & K2 ⊢ V1 [0, e - 1] ▶ V2 &
-                               L1 = K1. 𝕓{I} V1.
+                               L1 = K1. ⓑ{I} V1.
 /2 width=5/ qed-.
 
 fact ltps_inv_tps12_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → 0 < d →
-                         ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
+                         ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
                          ∃∃K1,V1. K1 [d - 1, e] ▶ K2 &
                                   K2 ⊢ V1 [d - 1, e] ▶ V2 &
-                                  L1 = K1. 𝕓{I} V1.
+                                  L1 = K1. ⓑ{I} V1.
 #d #e #L1 #L2 * -d -e -L1 -L2
 [ #d #e #_ #I #K2 #V2 #H destruct
 | #L #I #V #H elim (lt_refl_false … H)
@@ -160,10 +160,10 @@ fact ltps_inv_tps12_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → 0 < d →
 ]
 qed.
 
-lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ▶ K2. 𝕓{I} V2 → 0 < d →
+lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ▶ K2. ⓑ{I} V2 → 0 < d →
                       ∃∃K1,V1. K1 [d - 1, e] ▶ K2 &
                                   K2 ⊢ V1 [d - 1, e] ▶ V2 &
-                                  L1 = K1. 𝕓{I} V1.
+                                  L1 = K1. ⓑ{I} V1.
 /2 width=3/ qed-.
 
 (* Basic_1: removed theorems 27:
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_tps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_tps.ma
index 473f813b6..e8dfe59af 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_tps.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/ltps_tps.ma
@@ -57,7 +57,7 @@ lemma ltps_tps_conf: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
   ]
 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
   elim (IHVW2 … HL01) -IHVW2 #V #HV2 #HVW2
-  elim (IHTU2 (L1. 𝕓{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL01 /3 width=5/
+  elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL01 /3 width=5/
 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01
   elim (IHVW2 … HL01) -IHVW2
   elim (IHTU2 … HL01) -IHTU2 -HL01 /3 width=5/
@@ -104,7 +104,7 @@ lemma ltps_tps_trans: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
   ]
 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
   elim (IHVW2 … HL10) -IHVW2 #V #HV2 #HVW2
-  elim (IHTU2 (L1. 𝕓{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL10 /3 width=5/
+  elim (IHTU2 (L1. ⓑ{I} V) (d1 + 1) e1 ?) -IHTU2 /2 width=1/ -HL10 /3 width=5/
 | #L0 #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10
   elim (IHVW2 … HL10) -IHVW2
   elim (IHTU2 … HL10) -IHTU2 -HL10 /3 width=5/
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma
index 8a5dc13d0..11edc90b1 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps.ma
@@ -18,15 +18,15 @@ include "Basic_2/substitution/ldrop.ma".
 (* PARALLEL SUBSTITUTION ON TERMS *******************************************)
 
 inductive tps: nat → nat → lenv → relation term ≝
-| tps_atom : ∀L,I,d,e. tps d e L (𝕒{I}) (𝕒{I})
+| tps_atom : ∀L,I,d,e. tps d e L (⓪{I}) (⓪{I})
 | tps_subst: ∀L,K,V,W,i,d,e. d ≤ i → i < d + e →
-             ⇩[0, i] L ≡ K. 𝕓{Abbr} V → ⇧[0, i + 1] V ≡ W → tps d e L (#i) W
+             ⇩[0, i] L ≡ K. ⓓV → ⇧[0, i + 1] V ≡ W → tps d e L (#i) W
 | tps_bind : ∀L,I,V1,V2,T1,T2,d,e.
-             tps d e L V1 V2 → tps (d + 1) e (L. 𝕓{I} V2) T1 T2 →
-             tps d e L (𝕓{I} V1. T1) (𝕓{I} V2. T2)
+             tps d e L V1 V2 → tps (d + 1) e (L. ⓑ{I} V2) T1 T2 →
+             tps d e L (ⓑ{I} V1. T1) (ⓑ{I} V2. T2)
 | tps_flat : ∀L,I,V1,V2,T1,T2,d,e.
              tps d e L V1 V2 → tps d e L T1 T2 →
-             tps d e L (𝕗{I} V1. T1) (𝕗{I} V2. T2)
+             tps d e L (ⓕ{I} V1. T1) (ⓕ{I} V2. T2)
 .
 
 interpretation "parallel substritution (term)"
@@ -51,7 +51,7 @@ lemma tps_refl: ∀T,L,d,e. L ⊢ T [d, e] ▶ T.
 qed.
 
 (* Basic_1: was: subst1_ex *)
-lemma tps_full: ∀K,V,T1,L,d. ⇩[0, d] L ≡ (K. 𝕓{Abbr} V) →
+lemma tps_full: ∀K,V,T1,L,d. ⇩[0, d] L ≡ (K. ⓓV) →
                 ∃∃T2,T. L ⊢ T1 [d, 1] ▶ T2 & ⇧[d, 1] T ≡ T2.
 #K #V #T1 elim T1 -T1
 [ * #i #L #d #HLK /2 width=4/
@@ -61,7 +61,7 @@ lemma tps_full: ∀K,V,T1,L,d. ⇩[0, d] L ≡ (K. 𝕓{Abbr} V) →
   elim (lift_split … HVW i i ? ? ?) // /3 width=4/
 | * #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
   elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
-  [ elim (IHU1 (L. 𝕓{I} W2) (d+1) ?) -IHU1 /2 width=1/ -HLK /3 width=8/
+  [ elim (IHU1 (L. ⓑ{I} W2) (d+1) ?) -IHU1 /2 width=1/ -HLK /3 width=8/
   | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8/
   ]
 ]
@@ -115,7 +115,7 @@ lemma tps_split_up: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶ T2 → ∀i. d ≤ i →
   elim (IHV12 i ? ?) -IHV12 // #V #HV1 #HV2
   elim (IHT12 (i + 1) ? ?) -IHT12 /2 width=1/
   -Hdi -Hide >arith_c1x #T #HT1 #HT2
-  lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /3 width=5/
+  lapply (tps_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /3 width=5/
 | #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #i #Hdi #Hide
   elim (IHV12 i ? ?) -IHV12 // elim (IHT12 i ? ?) -IHT12 //
   -Hdi -Hide /3 width=5/
@@ -124,10 +124,10 @@ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-fact tps_inv_atom1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶ T2 → ∀I. T1 = 𝕒{I} →
-                        T2 = 𝕒{I} ∨
+fact tps_inv_atom1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶ T2 → ∀I. T1 = ⓪{I} →
+                        T2 = ⓪{I} ∨
                         ∃∃K,V,i. d ≤ i & i < d + e &
-                                 ⇩[O, i] L ≡ K. 𝕓{Abbr} V &
+                                 ⇩[O, i] L ≡ K. ⓓV &
                                  ⇧[O, i + 1] V ≡ T2 &
                                  I = LRef i.
 #L #T1 #T2 #d #e * -L -T1 -T2 -d -e
@@ -138,10 +138,10 @@ fact tps_inv_atom1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶ T2 → ∀I. T1 = 
 ]
 qed.
 
-lemma tps_inv_atom1: ∀L,T2,I,d,e. L ⊢ 𝕒{I} [d, e] ▶ T2 →
-                     T2 = 𝕒{I} ∨
+lemma tps_inv_atom1: ∀L,T2,I,d,e. L ⊢ ⓪{I} [d, e] ▶ T2 →
+                     T2 = ⓪{I} ∨
                      ∃∃K,V,i. d ≤ i & i < d + e &
-                              ⇩[O, i] L ≡ K. 𝕓{Abbr} V &
+                              ⇩[O, i] L ≡ K. ⓓV &
                               ⇧[O, i + 1] V ≡ T2 &
                               I = LRef i.
 /2 width=3/ qed-.
@@ -158,7 +158,7 @@ qed-.
 lemma tps_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ▶ T2 →
                      T2 = #i ∨
                      ∃∃K,V. d ≤ i & i < d + e &
-                            ⇩[O, i] L ≡ K. 𝕓{Abbr} V &
+                            ⇩[O, i] L ≡ K. ⓓV &
                             ⇧[O, i + 1] V ≡ T2.
 #L #T2 #i #d #e #H
 elim (tps_inv_atom1 … H) -H /2 width=1/
@@ -172,10 +172,10 @@ elim (tps_inv_atom1 … H) -H //
 qed-.
 
 fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ▶ U2 →
-                        ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
+                        ∀I,V1,T1. U1 = ⓑ{I} V1. T1 →
                         ∃∃V2,T2. L ⊢ V1 [d, e] ▶ V2 & 
-                                 L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ▶ T2 &
-                                 U2 =  𝕓{I} V2. T2.
+                                 L. ⓑ{I} V2 ⊢ T1 [d + 1, e] ▶ T2 &
+                                 U2 =  ⓑ{I} V2. T2.
 #d #e #L #U1 #U2 * -d -e -L -U1 -U2
 [ #L #k #d #e #I #V1 #T1 #H destruct
 | #L #K #V #W #i #d #e #_ #_ #_ #_ #I #V1 #T1 #H destruct
@@ -184,16 +184,16 @@ fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ▶ U2 →
 ]
 qed.
 
-lemma tps_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ▶ U2 →
+lemma tps_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓑ{I} V1. T1 [d, e] ▶ U2 →
                      ∃∃V2,T2. L ⊢ V1 [d, e] ▶ V2 & 
-                              L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ▶ T2 &
-                              U2 =  𝕓{I} V2. T2.
+                              L. ⓑ{I} V2 ⊢ T1 [d + 1, e] ▶ T2 &
+                              U2 =  ⓑ{I} V2. T2.
 /2 width=3/ qed-.
 
 fact tps_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ▶ U2 →
-                        ∀I,V1,T1. U1 = 𝕗{I} V1. T1 →
+                        ∀I,V1,T1. U1 = ⓕ{I} V1. T1 →
                         ∃∃V2,T2. L ⊢ V1 [d, e] ▶ V2 & L ⊢ T1 [d, e] ▶ T2 &
-                                 U2 =  𝕗{I} V2. T2.
+                                 U2 =  ⓕ{I} V2. T2.
 #d #e #L #U1 #U2 * -d -e -L -U1 -U2
 [ #L #k #d #e #I #V1 #T1 #H destruct
 | #L #K #V #W #i #d #e #_ #_ #_ #_ #I #V1 #T1 #H destruct
@@ -202,9 +202,9 @@ fact tps_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ▶ U2 →
 ]
 qed.
 
-lemma tps_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ▶ U2 →
+lemma tps_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 [d, e] ▶ U2 →
                      ∃∃V2,T2. L ⊢ V1 [d, e] ▶ V2 & L ⊢ T1 [d, e] ▶ T2 &
-                              U2 =  𝕗{I} V2. T2.
+                              U2 =  ⓕ{I} V2. T2.
 /2 width=3/ qed-.
 
 fact tps_inv_refl_O2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶ T2 → e = 0 → T1 = T2.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma
index 78c324e46..e453c4099 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_lift.ma
@@ -20,7 +20,7 @@ include "Basic_2/substitution/tps.ma".
 (* Advanced inversion lemmas ************************************************)
 
 fact tps_inv_refl_SO2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶ T2 → e = 1 →
-                           ∀K,V. ⇩[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
+                           ∀K,V. ⇩[0, d] L ≡ K. ⓛV → T1 = T2.
 #L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e
 [ //
 | #L #K0 #V0 #W #i #d #e #Hdi #Hide #HLK0 #_ #H destruct
@@ -34,7 +34,7 @@ fact tps_inv_refl_SO2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ▶ T2 → e = 1 →
 qed.
 
 lemma tps_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ▶ T2 →
-                        ∀K,V. ⇩[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
+                        ∀K,V. ⇩[0, d] L ≡ K. ⓛV → T1 = T2.
 /2 width=8/ qed-.
 
 (* Relocation properties ****************************************************)
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_tps.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_tps.ma
index f4ee71857..17346f53a 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_tps.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/tps_tps.ma
@@ -33,11 +33,11 @@ theorem tps_conf_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ▶ T1 →
   ]
 | #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
   elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
-  lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V1) ?) -HT02 /2 width=1/ #HT02
+  lapply (tps_lsubs_conf … HT02 (L. ⓑ{I} V1) ?) -HT02 /2 width=1/ #HT02
   elim (IHV01 … HV02) -V0 #V #HV1 #HV2
   elim (IHT01 … HT02) -T0 #T #HT1 #HT2
-  lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /2 width=1/
-  lapply (tps_lsubs_conf … HT2 (L. 𝕓{I} V) ?) -HT2 /3 width=5/
+  lapply (tps_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
+  lapply (tps_lsubs_conf … HT2 (L. ⓑ{I} V) ?) -HT2 /3 width=5/
 | #L #I #V0 #V1 #T0 #T1 #d1 #e1 #_ #_ #IHV01 #IHT01 #X #d2 #e2 #HX
   elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
   elim (IHV01 … HV02) -V0
@@ -71,8 +71,8 @@ theorem tps_conf_neq: ∀L1,T0,T1,d1,e1. L1 ⊢ T0 [d1, e1] ▶ T1 →
   elim (IHV01 … HV02 H) -V0 #V #HV1 #HV2
   elim (IHT01 … HT02 ?) -T0
   [ -H #T #HT1 #HT2
-    lapply (tps_lsubs_conf … HT1 (L2. 𝕓{I} V) ?) -HT1 /2 width=1/
-    lapply (tps_lsubs_conf … HT2 (L1. 𝕓{I} V) ?) -HT2 /2 width=1/ /3 width=5/
+    lapply (tps_lsubs_conf … HT1 (L2. ⓑ{I} V) ?) -HT1 /2 width=1/
+    lapply (tps_lsubs_conf … HT2 (L1. ⓑ{I} V) ?) -HT2 /2 width=1/ /3 width=5/
   | -HV1 -HV2 >plus_plus_comm_23 >plus_plus_comm_23 in ⊢ (? ? %); elim H -H #H
     [ @or_introl | @or_intror ] /2 by monotonic_le_plus_l/ (**) (* /3 / is too slow *)
   ]
@@ -100,9 +100,9 @@ theorem tps_trans_ge: ∀L,T1,T0,d,e. L ⊢ T1 [d, e] ▶ T0 →
   <(tps_inv_lift1_eq … HVT2 … HVW) -HVT2 /2 width=4/
 | #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
   elim (tps_inv_bind1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct
-  lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V0) ?) -HT02 /2 width=1/ #HT02
+  lapply (tps_lsubs_conf … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
   lapply (IHT10 … HT02 He) -T0 #HT12
-  lapply (tps_lsubs_conf … HT12 (L. 𝕓{I} V2) ?) -HT12 /2 width=1/ /3 width=1/
+  lapply (tps_lsubs_conf … HT12 (L. ⓑ{I} V2) ?) -HT12 /2 width=1/ /3 width=1/
 | #L #I #V1 #V0 #T1 #T0 #d #e #_ #_ #IHV10 #IHT10 #X #H #He
   elim (tps_inv_flat1 … H) -H #V2 #T2 #HV02 #HT02 #H destruct /3 width=1/
 ]
@@ -119,11 +119,11 @@ theorem tps_trans_down: ∀L,T1,T0,d1,e1. L ⊢ T1 [d1, e1] ▶ T0 →
   <(tps_inv_lift1_eq … HWT2 … HVW) -HWT2 /4 width=4/
 | #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
   elim (tps_inv_bind1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
-  lapply (tps_lsubs_conf … HT02 (L. 𝕓{I} V0) ?) -HT02 /2 width=1/ #HT02
+  lapply (tps_lsubs_conf … HT02 (L. ⓑ{I} V0) ?) -HT02 /2 width=1/ #HT02
   elim (IHV10 … HV02 ?) -IHV10 -HV02 // #V
   elim (IHT10 … HT02 ?) -T0 /2 width=1/ #T #HT1 #HT2
-  lapply (tps_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /2 width=1/
-  lapply (tps_lsubs_conf … HT2 (L. 𝕓{I} V2) ?) -HT2 /2 width=1/ /3 width=6/
+  lapply (tps_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/
+  lapply (tps_lsubs_conf … HT2 (L. ⓑ{I} V2) ?) -HT2 /2 width=1/ /3 width=6/
 | #L #I #V1 #V0 #T1 #T0 #d1 #e1 #_ #_ #IHV10 #IHT10 #X #d2 #e2 #HX #de2d1
   elim (tps_inv_flat1 … HX) -HX #V2 #T2 #HV02 #HT02 #HX destruct
   elim (IHV10 … HV02 ?) -V0 //
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift.ma
index 895706ef6..ec2d6c373 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift.ma
@@ -30,15 +30,15 @@ lemma delift_lsubs_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≡ T2 →
 qed.
 
 lemma delift_bind: ∀I,L,V1,V2,T1,T2,d,e.
-                   L ⊢ V1 [d, e] ≡ V2 → L. 𝕓{I} V2 ⊢ T1 [d+1, e] ≡ T2 →
-                   L ⊢ 𝕓{I} V1. T1 [d, e] ≡ 𝕓{I} V2. T2.
+                   L ⊢ V1 [d, e] ≡ V2 → L. ⓑ{I} V2 ⊢ T1 [d+1, e] ≡ T2 →
+                   L ⊢ ⓑ{I} V1. T1 [d, e] ≡ ⓑ{I} V2. T2.
 #I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * #T #HT1 #HT2
-lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V) ?) -HT1 /2 width=1/ /3 width=5/
+lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V) ?) -HT1 /2 width=1/ /3 width=5/
 qed.
 
 lemma delift_flat: ∀I,L,V1,V2,T1,T2,d,e.
                    L ⊢ V1 [d, e] ≡ V2 → L ⊢ T1 [d, e] ≡ T2 →
-                   L ⊢ 𝕗{I} V1. T1 [d, e] ≡ 𝕗{I} V2. T2.
+                   L ⊢ ⓕ{I} V1. T1 [d, e] ≡ ⓕ{I} V2. T2.
 #I #L #V1 #V2 #T1 #T2 #d #e * #V #HV1 #HV2 * /3 width=5/
 qed.
 
@@ -56,20 +56,20 @@ lemma delift_fwd_gref1: ∀L,U2,d,e,p. L ⊢ §p [d, e] ≡ U2 → U2 = §p.
 >(lift_inv_gref2 … HU2) -HU2 //
 qed-.
 
-lemma delift_fwd_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ 𝕓{I} V1. T1 [d, e] ≡ U2 →
+lemma delift_fwd_bind1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓑ{I} V1. T1 [d, e] ≡ U2 →
                         ∃∃V2,T2. L ⊢ V1 [d, e] ≡ V2 &
-                                 L. 𝕓{I} V2 ⊢ T1 [d+1, e] ≡ T2 &
-                                 U2 = 𝕓{I} V2. T2.
+                                 L. ⓑ{I} V2 ⊢ T1 [d+1, e] ≡ T2 &
+                                 U2 = ⓑ{I} V2. T2.
 #I #L #V1 #T1 #U2 #d #e * #U #HU #HU2
 elim (tpss_inv_bind1 … HU) -HU #V #T #HV1 #HT1 #X destruct
 elim (lift_inv_bind2 … HU2) -HU2 #V2 #T2 #HV2 #HT2
-lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
+lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
 qed-.
 
-lemma delift_fwd_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ 𝕗{I} V1. T1 [d, e] ≡ U2 →
+lemma delift_fwd_flat1: ∀I,L,V1,T1,U2,d,e. L ⊢ ⓕ{I} V1. T1 [d, e] ≡ U2 →
                         ∃∃V2,T2. L ⊢ V1 [d, e] ≡ V2 &
                                  L ⊢ T1 [d, e] ≡ T2 &
-                                 U2 = 𝕗{I} V2. T2.
+                                 U2 = ⓕ{I} V2. T2.
 #I #L #V1 #T1 #U2 #d #e * #U #HU #HU2
 elim (tpss_inv_flat1 … HU) -HU #V #T #HV1 #HT1 #X destruct
 elim (lift_inv_flat2 … HU2) -HU2 /3 width=5/
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift_lift.ma
index e725d65da..a02d3db2c 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/delift_lift.ma
@@ -31,7 +31,7 @@ qed-.
 
 lemma delift_fwd_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 →
                            d ≤ i → i < d + e →
-                           ∃∃K,V1,V2. ⇩[0, i] L ≡ K. 𝕓{Abbr} V1 &
+                           ∃∃K,V1,V2. ⇩[0, i] L ≡ K. ⓓV1 &
                                       K ⊢ V1 [0, d + e - i - 1] ≡ V2 &
                                       ⇧[0, d] V2 ≡ U2.
 #L #U2 #d #e #i * #U #HU #HU2 #Hdi #Hide
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma
index 254006f1c..78f4dd6af 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ldrops.ma
@@ -50,11 +50,11 @@ lemma ldrops_inv_cons: ∀L1,L2,d,e,des. ⇩*[{d, e} :: des] L1 ≡ L2 →
 /2 width=3/ qed-.
 
 lemma ldrops_inv_skip2: ∀I,des,i,des2. des ▭ i ≡ des2 →
-                        ∀L1,K2,V2. ⇩*[des2] L1 ≡ K2. 𝕓{I} V2 →
+                        ∀L1,K2,V2. ⇩*[des2] L1 ≡ K2. ⓑ{I} V2 →
                         ∃∃K1,V1,des1. des + 1 ▭ i + 1 ≡ des1 + 1 &
                                       ⇩*[des1] K1 ≡ K2 &
                                       ⇧*[des1] V2 ≡ V1 &
-                                      L1 = K1. 𝕓{I} V1.
+                                      L1 = K1. ⓑ{I} V1.
 #I #des #i #des2 #H elim H -des -i -des2
 [ #i #L1 #K2 #V2 #H
   >(ldrops_inv_nil … H) -L1 /2 width=7/
@@ -73,7 +73,7 @@ qed-.
 (* Basic properties *********************************************************)
 
 lemma ldrops_skip: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2 ≡ V1 →
-                   ∀I. ⇩*[des + 1] L1. 𝕓{I} V1 ≡ L2. 𝕓{I} V2.
+                   ∀I. ⇩*[des + 1] L1. ⓑ{I} V1 ≡ L2. ⓑ{I} V2.
 #L1 #L2 #des #H elim H -L1 -L2 -des
 [ #L #V1 #V2 #HV12 #I
   >(lifts_inv_nil … HV12) -HV12 //
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma
index 27ddc5174..40f4325b1 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts.ma
@@ -81,9 +81,9 @@ lemma lifts_inv_gref1: ∀T2,p,des. ⇧*[des] §p ≡ T2 → T2 = §p.
 qed-.
 
 (* Basic_1: was: lift1_bind *)
-lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇧*[des] 𝕓{I} V1. U1 ≡ T2 →
+lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇧*[des] ⓑ{I} V1. U1 ≡ T2 →
                        ∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[des + 1] U1 ≡ U2 &
-                                T2 = 𝕓{I} V2. U2.
+                                T2 = ⓑ{I} V2. U2.
 #I #T2 #des elim des -des
 [ #V1 #U1 #H
   <(lifts_inv_nil … H) -H /2 width=5/
@@ -96,9 +96,9 @@ lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇧*[des] 𝕓{I} V1. U1 ≡ T2 →
 qed-.
 
 (* Basic_1: was: lift1_flat *)
-lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇧*[des] 𝕗{I} V1. U1 ≡ T2 →
+lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇧*[des] ⓕ{I} V1. U1 ≡ T2 →
                        ∃∃V2,U2. ⇧*[des] V1 ≡ V2 & ⇧*[des] U1 ≡ U2 &
-                                T2 = 𝕗{I} V2. U2.
+                                T2 = ⓕ{I} V2. U2.
 #I #T2 #des elim des -des
 [ #V1 #U1 #H
   <(lifts_inv_nil … H) -H /2 width=5/
@@ -124,7 +124,7 @@ qed-.
 
 lemma lifts_bind: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
                   ∀T1. ⇧*[des + 1] T1 ≡ T2 →
-                  ⇧*[des] 𝕓{I} V1. T1 ≡ 𝕓{I} V2. T2.
+                  ⇧*[des] ⓑ{I} V1. T1 ≡ ⓑ{I} V2. T2.
 #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
 [ #V #T1 #H >(lifts_inv_nil … H) -H //
 | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
@@ -134,7 +134,7 @@ qed.
 
 lemma lifts_flat: ∀I,T2,V1,V2,des. ⇧*[des] V1 ≡ V2 →
                   ∀T1. ⇧*[des] T1 ≡ T2 →
-                  ⇧*[des] 𝕗{I} V1. T1 ≡ 𝕗{I} V2. T2.
+                  ⇧*[des] ⓕ{I} V1. T1 ≡ ⓕ{I} V2. T2.
 #I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
 [ #V #T1 #H >(lifts_inv_nil … H) -H //
 | #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma
index 7c3c7640f..f3ec86b2d 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/lifts_vector.ma
@@ -35,8 +35,8 @@ axiom lifts_inv_applv1: ∀V1s,U1,T2,des. ⇧*[des] Ⓐ V1s. U1 ≡ T2 →
 
 (* Basic properties *********************************************************)
 
-lemma liftsv_applv: ∀V1s,V2s,des. ⇧*[des] V1s ≡ V2s →
-                    ∀T1,T2. ⇧*[des] T1 ≡ T2 →
-                    ⇧*[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.
+lemma lifts_applv: ∀V1s,V2s,des. ⇧*[des] V1s ≡ V2s →
+                   ∀T1,T2. ⇧*[des] T1 ≡ T2 →
+                   ⇧*[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.
 #V1s #V2s #des #H elim H -V1s -V2s // /3 width=1/
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma
index 6ede048c5..28e9608e1 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss.ma
@@ -63,10 +63,10 @@ lemma ltpss_inv_atom2: ∀d,e,L1. L1 [d, e] ▶* ⋆ → L1 = ⋆.
 /2 width=5/ qed-.
 (*
 fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → d = 0 → 0 < e →
-                         ∀K2,I,V2. L2 = K2. 𝕓{I} V2 →
+                         ∀K2,I,V2. L2 = K2. ⓑ{I} V2 →
                          ∃∃K1,V1. K1 [0, e - 1] ▶ K2 &
                                   K2 ⊢ V1 [0, e - 1] ▶ V2 &
-                                  L1 = K1. 𝕓{I} V1.
+                                  L1 = K1. ⓑ{I} V1.
 #d #e #L1 #L2 * -d e L1 L2
 [ #d #e #_ #_ #K1 #I #V1 #H destruct
 | #L1 #I #V #_ #H elim (lt_refl_false … H)
@@ -75,16 +75,16 @@ fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → d = 0 → 0 < e →
 ]
 qed.
 
-lemma ltps_inv_tps22: ∀e,L1,K2,I,V2. L1 [0, e] ▶ K2. 𝕓{I} V2 → 0 < e →
+lemma ltps_inv_tps22: ∀e,L1,K2,I,V2. L1 [0, e] ▶ K2. ⓑ{I} V2 → 0 < e →
                       ∃∃K1,V1. K1 [0, e - 1] ▶ K2 & K2 ⊢ V1 [0, e - 1] ▶ V2 &
-                               L1 = K1. 𝕓{I} V1.
+                               L1 = K1. ⓑ{I} V1.
 /2 width=5/ qed.
 
 fact ltps_inv_tps12_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → 0 < d →
-                         ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
+                         ∀I,K2,V2. L2 = K2. ⓑ{I} V2 →
                          ∃∃K1,V1. K1 [d - 1, e] ▶ K2 &
                                   K2 ⊢ V1 [d - 1, e] ▶ V2 &
-                                  L1 = K1. 𝕓{I} V1.
+                                  L1 = K1. ⓑ{I} V1.
 #d #e #L1 #L2 * -d e L1 L2
 [ #d #e #_ #I #K2 #V2 #H destruct
 | #L #I #V #H elim (lt_refl_false … H)
@@ -93,9 +93,9 @@ fact ltps_inv_tps12_aux: ∀d,e,L1,L2. L1 [d, e] ▶ L2 → 0 < d →
 ]
 qed.
 
-lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ▶ K2. 𝕓{I} V2 → 0 < d →
+lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ▶ K2. ⓑ{I} V2 → 0 < d →
                       ∃∃K1,V1. K1 [d - 1, e] ▶ K2 &
                                   K2 ⊢ V1 [d - 1, e] ▶ V2 &
-                                  L1 = K1. 𝕓{I} V1.
+                                  L1 = K1. ⓑ{I} V1.
 /2 width=1/ qed.
 *)
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ltpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ltpss.ma
index e9995db70..7091e0803 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ltpss.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_ltpss.ma
@@ -24,7 +24,7 @@ theorem ltpss_trans_eq: ∀L1,L,L2,d,e.
 
 lemma ltpss_tpss2: ∀L1,L2,I,V1,V2,e.
                    L1 [0, e] ▶* L2 → L2 ⊢ V1 [0, e] ▶* V2 →
-                   L1. 𝕓{I} V1 [0, e + 1] ▶* L2. 𝕓{I} V2.
+                   L1. ⓑ{I} V1 [0, e + 1] ▶* L2. ⓑ{I} V2.
 #L1 #L2 #I #V1 #V2 #e #HL12 #H @(tpss_ind … H) -V2
 [ /2 width=1/
 | #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2 width=1/
@@ -33,14 +33,14 @@ qed.
 
 lemma ltpss_tpss2_lt: ∀L1,L2,I,V1,V2,e.
                       L1 [0, e - 1] ▶* L2 → L2 ⊢ V1 [0, e - 1] ▶* V2 →
-                      0 < e → L1. 𝕓{I} V1 [0, e] ▶* L2. 𝕓{I} V2.
+                      0 < e → L1. ⓑ{I} V1 [0, e] ▶* L2. ⓑ{I} V2.
 #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
 >(plus_minus_m_m e 1) // /2 width=1/
 qed.
 
 lemma ltpss_tpss1: ∀L1,L2,I,V1,V2,d,e.
                    L1 [d, e] ▶* L2 → L2 ⊢ V1 [d, e] ▶* V2 →
-                   L1. 𝕓{I} V1 [d + 1, e] ▶* L2. 𝕓{I} V2.
+                   L1. ⓑ{I} V1 [d + 1, e] ▶* L2. ⓑ{I} V2.
 #L1 #L2 #I #V1 #V2 #d #e #HL12 #H @(tpss_ind … H) -V2
 [ /2 width=1/
 | #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2 width=1/
@@ -49,7 +49,7 @@ qed.
 
 lemma ltpss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e.
                       L1 [d - 1, e] ▶* L2 → L2 ⊢ V1 [d - 1, e] ▶* V2 →
-                      0 < d → L1. 𝕓{I} V1 [d, e] ▶* L2. 𝕓{I} V2.
+                      0 < d → L1. ⓑ{I} V1 [d, e] ▶* L2. ⓑ{I} V2.
 #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
 >(plus_minus_m_m d 1) // /2 width=1/
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma
index 5dbe0dea1..24f1a595e 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_tpss.ma
@@ -105,7 +105,7 @@ lemma ltpss_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ▶ T2 →
 
 lemma ltpss_tps2: ∀L1,L2,I,e.
                   L1 [0, e] ▶* L2 → ∀V1,V2. L2 ⊢ V1 [0, e] ▶ V2 →
-                  L1. 𝕓{I} V1 [0, e + 1] ▶* L2. 𝕓{I} V2.
+                  L1. ⓑ{I} V1 [0, e + 1] ▶* L2. ⓑ{I} V2.
 #L1 #L2 #I #e #H @(ltpss_ind … H) -L2
 [ /3 width=1/
 | #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
@@ -117,14 +117,14 @@ qed.
 
 lemma ltpss_tps2_lt: ∀L1,L2,I,V1,V2,e.
                      L1 [0, e - 1] ▶* L2 → L2 ⊢ V1 [0, e - 1] ▶ V2 →
-                     0 < e → L1. 𝕓{I} V1 [0, e] ▶* L2. 𝕓{I} V2.
+                     0 < e → L1. ⓑ{I} V1 [0, e] ▶* L2. ⓑ{I} V2.
 #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
 >(plus_minus_m_m e 1) // /2 width=1/
 qed.
 
 lemma ltpss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ▶* L2 →
                   ∀V1,V2. L2 ⊢ V1 [d, e] ▶ V2 →
-                  L1. 𝕓{I} V1 [d + 1, e] ▶* L2. 𝕓{I} V2.
+                  L1. ⓑ{I} V1 [d + 1, e] ▶* L2. ⓑ{I} V2.
 #L1 #L2 #I #d #e #H @(ltpss_ind … H) -L2
 [ /3 width=1/
 | #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
@@ -136,16 +136,16 @@ qed.
 
 lemma ltpss_tps1_lt: ∀L1,L2,I,V1,V2,d,e.
                      L1 [d - 1, e] ▶* L2 → L2 ⊢ V1 [d - 1, e] ▶ V2 →
-                     0 < d → L1. 𝕓{I} V1 [d, e] ▶* L2. 𝕓{I} V2.
+                     0 < d → L1. ⓑ{I} V1 [d, e] ▶* L2. ⓑ{I} V2.
 #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
 >(plus_minus_m_m d 1) // /2 width=1/
 qed.
 
 (* Advanced forward lemmas **************************************************)
 
-lemma ltpss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. 𝕓{I} V1 [0, e] ▶* L2 →
+lemma ltpss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. ⓑ{I} V1 [0, e] ▶* L2 →
                         ∃∃K2,V2. K1 [0, e - 1] ▶* K2 & K1 ⊢ V1 [0, e - 1] ▶* V2 &
-                                 L2 = K2. 𝕓{I} V2.
+                                 L2 = K2. ⓑ{I} V2.
 #e #K1 #I #V1 #L2 #He #H @(ltpss_ind … H) -L2
 [ /2 width=5/
 | #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
@@ -155,10 +155,10 @@ lemma ltpss_fwd_tpss21: ∀e,K1,I,V1,L2. 0 < e → K1. 𝕓{I} V1 [0, e] ▶* L2
 ]
 qed-.
 
-lemma ltpss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. 𝕓{I} V1 [d, e] ▶* L2 →
+lemma ltpss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. ⓑ{I} V1 [d, e] ▶* L2 →
                         ∃∃K2,V2. K1 [d - 1, e] ▶* K2 &
                                  K1 ⊢ V1 [d - 1, e] ▶* V2 &
-                                 L2 = K2. 𝕓{I} V2.
+                                 L2 = K2. ⓑ{I} V2.
 #d #e #K1 #I #V1 #L2 #Hd #H @(ltpss_ind … H) -L2
 [ /2 width=5/
 | #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma
index 0db2e9395..16a0d3e4d 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss.ma
@@ -44,22 +44,22 @@ lemma tpss_refl: ∀d,e,L,T. L ⊢ T [d, e] ▶* T.
 /2 width=1/ qed.
 
 lemma tpss_bind: ∀L,V1,V2,d,e. L ⊢ V1 [d, e] ▶* V2 →
-                 ∀I,T1,T2. L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ▶* T2 →
-                 L ⊢ 𝕓{I} V1. T1 [d, e] ▶* 𝕓{I} V2. T2.
+                 ∀I,T1,T2. L. ⓑ{I} V2 ⊢ T1 [d + 1, e] ▶* T2 →
+                 L ⊢ ⓑ{I} V1. T1 [d, e] ▶* ⓑ{I} V2. T2.
 #L #V1 #V2 #d #e #HV12 elim HV12 -V2
 [ #V2 #HV12 #I #T1 #T2 #HT12 elim HT12 -T2
   [ /3 width=5/
   | #T #T2 #_ #HT2 #IHT @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
   ]
 | #V #V2 #_ #HV12 #IHV #I #T1 #T2 #HT12
-  lapply (tpss_lsubs_conf … HT12 (L. 𝕓{I} V) ?) -HT12 /2 width=1/ #HT12
+  lapply (tpss_lsubs_conf … HT12 (L. ⓑ{I} V) ?) -HT12 /2 width=1/ #HT12
   lapply (IHV … HT12) -IHV -HT12 #HT12 @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
 ]
 qed.
 
 lemma tpss_flat: ∀L,I,V1,V2,T1,T2,d,e.
                  L ⊢ V1 [d, e] ▶ * V2 → L ⊢ T1 [d, e] ▶* T2 →
-                 L ⊢ 𝕗{I} V1. T1 [d, e] ▶* 𝕗{I} V2. T2.
+                 L ⊢ ⓕ{I} V1. T1 [d, e] ▶* ⓕ{I} V2. T2.
 #L #I #V1 #V2 #T1 #T2 #d #e #HV12 elim HV12 -V2
 [ #V2 #HV12 #HT12 elim HT12 -T2
   [ /3 width=1/
@@ -116,21 +116,21 @@ lemma tpss_inv_gref1: ∀L,T2,p,d,e. L ⊢ §p [d, e] ▶* T2 → T2 = §p.
 ]
 qed-.
 
-lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕓{I} V1. T1 [d, e] ▶* U2 →
+lemma tpss_inv_bind1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓑ{I} V1. T1 [d, e] ▶* U2 →
                       ∃∃V2,T2. L ⊢ V1 [d, e] ▶* V2 & 
-                               L. 𝕓{I} V2 ⊢ T1 [d + 1, e] ▶* T2 &
-                               U2 =  𝕓{I} V2. T2.
+                               L. ⓑ{I} V2 ⊢ T1 [d + 1, e] ▶* T2 &
+                               U2 =  ⓑ{I} V2. T2.
 #d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2
 [ /2 width=5/
 | #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
   elim (tps_inv_bind1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
-  lapply (tpss_lsubs_conf … HT1 (L. 𝕓{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
+  lapply (tpss_lsubs_conf … HT1 (L. ⓑ{I} V2) ?) -HT1 /2 width=1/ /3 width=5/
 ]
 qed-.
 
-lemma tpss_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ 𝕗{I} V1. T1 [d, e] ▶* U2 →
+lemma tpss_inv_flat1: ∀d,e,L,I,V1,T1,U2. L ⊢ ⓕ{I} V1. T1 [d, e] ▶* U2 →
                       ∃∃V2,T2. L ⊢ V1 [d, e] ▶* V2 & L ⊢ T1 [d, e] ▶* T2 &
-                               U2 =  𝕗{I} V2. T2.
+                               U2 =  ⓕ{I} V2. T2.
 #d #e #L #I #V1 #T1 #U2 #H @(tpss_ind … H) -U2
 [ /2 width=5/
 | #U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma
index 89c767133..748efd827 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_lift.ma
@@ -21,7 +21,7 @@ include "Basic_2/unfold/tpss.ma".
 
 lemma tpss_subst: ∀L,K,V,U1,i,d,e.
                   d ≤ i → i < d + e →
-                  ⇩[0, i] L ≡ K. 𝕓{Abbr} V → K ⊢ V [0, d + e - i - 1] ▶* U1 →
+                  ⇩[0, i] L ≡ K. ⓓV → K ⊢ V [0, d + e - i - 1] ▶* U1 →
                   ∀U2. ⇧[0, i + 1] U1 ≡ U2 → L ⊢ #i [d, e] ▶* U2.
 #L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(tpss_ind … H) -U1
 [ /3 width=4/
@@ -36,10 +36,10 @@ qed.
 
 (* Advanced inverion lemmas *************************************************)
 
-lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ 𝕒{I} [d, e] ▶* T2 →
-                      T2 = 𝕒{I} ∨
+lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ ⓪{I} [d, e] ▶* T2 →
+                      T2 = ⓪{I} ∨
                       ∃∃K,V1,V2,i. d ≤ i & i < d + e &
-                                   ⇩[O, i] L ≡ K. 𝕓{Abbr} V1 &
+                                   ⇩[O, i] L ≡ K. ⓓV1 &
                                    K ⊢ V1 [0, d + e - i - 1] ▶* V2 &
                                    ⇧[O, i + 1] V2 ≡ T2 &
                                    I = LRef i.
@@ -59,7 +59,7 @@ qed-.
 lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ▶* T2 →
                       T2 = #i ∨
                       ∃∃K,V1,V2. d ≤ i & i < d + e &
-                                 ⇩[O, i] L ≡ K. 𝕓{Abbr} V1 &
+                                 ⇩[O, i] L ≡ K. ⓓV1 &
                                  K ⊢ V1 [0, d + e - i - 1] ▶* V2 &
                                  ⇧[O, i + 1] V2 ≡ T2.
 #L #T2 #i #d #e #H
@@ -68,7 +68,7 @@ elim (tpss_inv_atom1 … H) -H /2 width=1/
 qed-.
 
 lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ▶* T2 →
-                         ∀K,V. ⇩[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
+                         ∀K,V. ⇩[0, d] L ≡ K. ⓛV → T1 = T2.
 #L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -T2 //
 #T #T2 #_ #HT2 #IHT <(tps_inv_refl_SO2 … HT2 … HLK) //
 qed-.
diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma
index b59015200..58b63cd01 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/tpss_ltps.ma
@@ -74,10 +74,10 @@ fact ltps_tps_trans_eq_aux: ∀Y1,X2,L1,T2,U2,d,e.
   lapply (IH … HV01 … HK01 ? ?) -IH -HV01 -HK01
   [1,3: // |2,4: skip | normalize /2 width=1/ | /3 width=6/ ]
 | #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct
-  lapply (tps_lsubs_conf … HT12 (L. 𝕓{I} V1) ?) -HT12 /2 width=1/ #HT12
+  lapply (tps_lsubs_conf … HT12 (L. ⓑ{I} V1) ?) -HT12 /2 width=1/ #HT12
   lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=2/ ] #HV12
-  lapply (IH … HT12 (L0. 𝕓{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
-  lapply (tpss_lsubs_conf … HT12 (L0. 𝕓{I} V2) ?) -HT12 /2 width=1/
+  lapply (IH … HT12 (L0. ⓑ{I} V1) ? ? ?) -IH -HT12 [1,3,5: /2 width=2/ |2,4: skip | normalize // ] -HL0 #HT12
+  lapply (tpss_lsubs_conf … HT12 (L0. ⓑ{I} V2) ?) -HT12 /2 width=1/
 | #L #I #V1 #V2 #T1 #T2 #d #e #HV12 #HT12 #L0 #HL0 #H1 #H2 destruct
   lapply (IH … HV12 … HL0 ? ?) -HV12 [1,3: // |2,4: skip |5: /2 width=3/ ]
   lapply (IH … HT12 … HL0 ? ?) -IH -HT12 [1,3,5: normalize // |2,4: skip ] -HL0 /2 width=1/
diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml b/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml
index 5a4cf8c49..a90d256fe 100644
--- a/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml
+++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa.conf.xml
@@ -16,6 +16,7 @@
     <key name="include">basics/pts.ma</key>
     <key name="ex">2 1</key>
     <key name="ex">2 2</key>
+    <key name="ex">2 3</key>
     <key name="ex">3 1</key>
     <key name="ex">3 2</key>
     <key name="ex">3 3</key>
diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma b/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma
index 48593d76e..1ff53beb4 100644
--- a/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa.ma
@@ -32,6 +32,14 @@ inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝
 
 interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1).
 
+(* multiple existental quantifier (2, 3) *)
+
+inductive ex2_3 (A0,A1,A2:Type[0]) (P0,P1:A0→A1→A2→Prop) : Prop ≝
+   | ex2_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → ex2_3 ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (2, 3)" 'Ex P0 P1 = (ex2_3 ? ? ? P0 P1).
+
 (* multiple existental quantifier (3, 1) *)
 
 inductive ex3_1 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝
diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma b/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma
index 20ab21e69..80c20da30 100644
--- a/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa_notation.ma
@@ -34,6 +34,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) }.
 
+(* multiple existental quantifier (2, 3) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) }.
+
 (* multiple existental quantifier (3, 1) *)
 
 notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile
index 9a7cdc1ec..10271b7ce 100644
--- a/matita/matita/contribs/lambda_delta/Makefile
+++ b/matita/matita/contribs/lambda_delta/Makefile
@@ -26,35 +26,35 @@ stats: $(PACKAGES:%=%.stats)
 %.stats: CHARS = $(shell cat $(MAS) | wc -c)
 
 %.stats:
-	@printf '\e[1;40;37m'
+	@printf '\x1B[1;40;37m'
 	@printf '%-15s %-42s' 'Statistics for:' $*	
-	@printf '\e[0m\n'	
-	@printf '\e[1;40;35m'
+	@printf '\x1B[0m\n'	
+	@printf '\x1B[1;40;35m'
 	@printf '%-8s %6i' Chars $(CHARS)
 	@printf '   %-8s %5i' Lines `cat $(MAS) | wc -l`
 	@printf '   %-6s %3i' Pages `echo $$(($(CHARS) / 5120))`
 	@printf '   %-10s' ''
-	@printf '\e[0m\n'
-	@printf '\e[1;40;36m'
+	@printf '\x1B[0m\n'
+	@printf '\x1B[1;40;36m'
 	@printf '%-8s %6i' Sources `ls $(MAS) | wc -l`
 	@printf '   %-40s' ''
 #	@printf '   %-8s %5i' Objs `ls *.vo | wc -l`
 #	@printf '   %-6s %3i' Files `ls *.v | wc -l`
-	@printf '\e[0m\n'	
-	@printf '\e[1;40;32m'
+	@printf '\x1B[0m\n'	
+	@printf '\x1B[1;40;32m'
 	@printf '%-8s %6i' Theorems `grep theorem $(MAS) | wc -l`
 	@printf '   %-8s %5i' Lemmas `grep lemma $(MAS) | wc -l`
 	@printf '   %-6s %3i' Facts `grep fact $(MAS) | wc -l`
 	@printf '   %-6s %3i' Proofs `grep qed $(MAS) | wc -l`
-	@printf '\e[0m\n'	
-	@printf '\e[1;40;33m'
+	@printf '\x1B[0m\n'	
+	@printf '\x1B[1;40;33m'
 	@printf '%-8s %6i' Defs `grep "definition\|let rec\|inductive\|record" $(MAS) | wc -l` 
 	@printf '   %-40s' ''
 #	@printf '   %-8s %5i' Local `grep "Local" *.v | wc -l`
-	@printf '\e[0m\n'
-	@printf '\e[1;40;31m'
+	@printf '\x1B[0m\n'
+	@printf '\x1B[1;40;31m'
 	@printf '%-8s %6i' Axioms `grep axiom $(MAS) | wc -l`
 	@printf '   %-8s %5i' Comments `grep "(\*[^*:]*$$" $(MAS) | wc -l`
 	@printf '   %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l`
 	@printf '   %-10s' ''
-	@printf '\e[0m\n'
+	@printf '\x1B[0m\n'
-- 
2.39.2