From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 31 Jan 2016 14:37:43 +0000 (+0000)
Subject: renaming ...
X-Git-Tag: make_still_working~654
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=e92beef4185d9c11884bcdb123429b1e7138e40c

renaming ...
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.etc
deleted file mode 100644
index 7a0cdfc92..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lenv/lenv_length.etc
+++ /dev/null
@@ -1,59 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "ground_2/ynat/ynat_lt.ma".
-include "basic_2/grammar/lenv.ma".
-
-(* LENGTH OF A LOCAL ENVIRONMENT ********************************************)
-
-let rec length L ≝ match L with
-[ LAtom       ⇒ 0
-| LPair L _ _ ⇒ ⫯(length L)
-].
-
-interpretation "length (local environment)" 'card L = (length L).
-
-(* Basic properties *********************************************************)
-
-lemma length_atom: |⋆| = 0.
-// qed.
-
-lemma length_pair: ∀I,L,V. |L.ⓑ{I}V| = ⫯|L|.
-// qed.
-
-lemma length_inj: ∀L. |L| < ∞.
-#L elim L -L /2 width=1 by ylt_succ_Y/
-qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma length_inv_zero_dx: ∀L. |L| = 0 → L = ⋆.
-* // #L #I #V >length_pair
-#H elim (ysucc_inv_O_dx … H)
-qed-.
-
-lemma length_inv_zero_sn: ∀L. yinj 0 = |L| → L = ⋆.
-/2 width=1 by length_inv_zero_dx/ qed-.
-
-lemma length_inv_pos_dx: ∀l,L. |L| = ⫯l →
-                         ∃∃I,K,V. |K| = l & L = K. ⓑ{I}V.
-#l * /3 width=5 by ysucc_inj, ex2_3_intro/
->length_atom #H elim (ysucc_inv_O_sn … H)
-qed-.
-
-lemma length_inv_pos_sn: ∀l,L. ⫯l = |L| →
-                         ∃∃I,K,V. l = |K| & L = K. ⓑ{I}V.
-#l #L #H lapply (sym_eq ??? H) -H 
-#H elim (length_inv_pos_dx … H) -H /2 width=5 by ex2_3_intro/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma
index 96dec98ba..7f44246c7 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/aarity.ma
@@ -39,7 +39,7 @@ fact destruct_apair_apair_aux: ∀A1,A2,B1,B2. ②B1.A1 = ②B2.A2 → B1 = B2 
 #A1 #A2 #B1 #B2 #H destruct /2 width=1 by conj/
 qed-.
 
-lemma discr_apair_xy_x: ∀A,B. ②B. A = B → ⊥.
+lemma discr_apair_xy_x: ∀A,B. ②B.A = B → ⊥.
 #A #B elim B -B
 [ #H destruct
 | #Y #X #IHY #_ #H elim (destruct_apair_apair_aux … H) -H /2 width=1 by/ (**) (* destruct lemma needed *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_restricted_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_restricted_weight.ma
index 3669ca151..fb2bcaf94 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_restricted_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_restricted_weight.ma
@@ -24,7 +24,7 @@ interpretation "weight (restricted closure)" 'Weight L T = (rfw L T).
 (* Basic properties *********************************************************)
 
 (* Basic_1: was: flt_shift *)
-lemma rfw_shift: ∀a,I,K,V,T. ♯{K.ⓑ{I}V, T} < ♯{K, ⓑ{a,I}V.T}.
+lemma rfw_shift: ∀p,I,K,V,T. ♯{K.ⓑ{I}V, T} < ♯{K, ⓑ{p,I}V.T}.
 normalize //
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
index d7c923dd4..5fb0671c2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/cl_weight.ma
@@ -26,7 +26,7 @@ interpretation "weight (closure)" 'Weight G L T = (fw G L T).
 (* Basic properties *********************************************************)
 
 (* Basic_1: was: flt_shift *)
-lemma fw_shift: ∀a,I,G,K,V,T. ♯{G, K.ⓑ{I}V, T} < ♯{G, K, ⓑ{a,I}V.T}.
+lemma fw_shift: ∀p,I,G,K,V,T. ♯{G, K.ⓑ{I}V, T} < ♯{G, K, ⓑ{p,I}V.T}.
 normalize //
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma
index 27d019994..c614e0f4e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/genv.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/lib/list.ma".
+include "ground_2/lib/list2.ma".
 include "basic_2/notation/constructors/star_0.ma".
 include "basic_2/notation/constructors/dxbind2_3.ma".
 include "basic_2/notation/constructors/dxabbr_2.ma".
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma
index cb69d3687..ab861be57 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/item.ma
@@ -44,8 +44,8 @@ inductive item2: Type[0] ≝
 
 (* Basic inversion lemmas ***************************************************)
 
-fact destruct_sort_sort_aux: ∀k1,k2. Sort k1 = Sort k2 → k1 = k2.
-#k1 #k2 #H destruct //
+fact destruct_sort_sort_aux: ∀s1,s2. Sort s1 = Sort s2 → s1 = s2.
+#s1 #s2 #H destruct //
 qed-.
 
 (* Basic properties *********************************************************)
@@ -70,9 +70,9 @@ qed-.
 
 (* Basic_1: was: kind_dec *)
 lemma eq_item2_dec: ∀I1,I2:item2. Decidable (I1 = I2).
-* [ #a1 ] #I1 * [1,3: #a2 ] #I2
+* [ #p1 ] #I1 * [1,3: #p2 ] #I2
 [2,3: @or_intror #H destruct
-| elim (eq_bool_dec a1 a2) #Ha
+| elim (eq_bool_dec p1 p2) #Hp
   [ elim (eq_bind2_dec I1 I2) /2 width=1 by or_introl/ #HI ]
   @or_intror #H destruct /2 width=1 by/
 | elim (eq_flat2_dec I1 I2) /2 width=1 by or_introl/ #HI
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma
new file mode 100644
index 000000000..29fee0ef1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/lenv_length.ma
@@ -0,0 +1,56 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/grammar/lenv.ma".
+
+(* LENGTH OF A LOCAL ENVIRONMENT ********************************************)
+
+let rec length L ≝ match L with
+[ LAtom       ⇒ 0
+| LPair L _ _ ⇒ ⫯(length L)
+].
+
+interpretation "length (local environment)" 'card L = (length L).
+
+(* Basic properties *********************************************************)
+
+lemma length_atom: |⋆| = 0.
+// qed.
+
+lemma length_pair: ∀I,L,V. |L.ⓑ{I}V| = ⫯|L|.
+// qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma length_inv_zero_dx: ∀L. |L| = 0 → L = ⋆.
+* // #L #I #V >length_pair
+#H destruct
+qed-.
+
+lemma length_inv_zero_sn: ∀L. 0 = |L| → L = ⋆.
+/2 width=1 by length_inv_zero_dx/ qed-.
+
+lemma length_inv_pos_dx: ∀n,L. |L| = ⫯n →
+                         ∃∃I,K,V. |K| = n & L = K. ⓑ{I}V.
+#n * /3 width=5 by injective_S, ex2_3_intro/
+>length_atom #H destruct
+qed-.
+
+lemma length_inv_pos_sn: ∀n,L. ⫯n = |L| →
+                         ∃∃I,K,V. n = |K| & L = K. ⓑ{I}V.
+#l #L #H lapply (sym_eq ??? H) -H 
+#H elim (length_inv_pos_dx … H) -H /2 width=5 by ex2_3_intro/
+qed-.
+
+(* Basic_2A1: removed theorems 1: length_inj *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma
index e70058dc9..ff00f4f84 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term.ma
@@ -46,7 +46,7 @@ interpretation "term construction (binary)"
    'SnItem2 I T1 T2 = (TPair I T1 T2).
 
 interpretation "term binding construction (binary)"
-   'SnBind2 a I T1 T2 = (TPair (Bind2 a I) T1 T2).
+   'SnBind2 p I T1 T2 = (TPair (Bind2 p I) T1 T2).
 
 interpretation "term positive binding construction (binary)"
    'SnBind2Pos I T1 T2 = (TPair (Bind2 true I) T1 T2).
@@ -58,16 +58,16 @@ interpretation "term flat construction (binary)"
    'SnFlat2 I T1 T2 = (TPair (Flat2 I) T1 T2).
 
 interpretation "sort (term)"
-   'Star k = (TAtom (Sort k)).
+   'Star s = (TAtom (Sort s)).
 
 interpretation "local reference (term)"
    'LRef i = (TAtom (LRef i)).
 
 interpretation "global reference (term)"
-   'GRef p = (TAtom (GRef p)).
+   'GRef l = (TAtom (GRef l)).
 
 interpretation "abbreviation (term)"
-   'SnAbbr a T1 T2 = (TPair (Bind2 a Abbr) T1 T2).
+   'SnAbbr p T1 T2 = (TPair (Bind2 p Abbr) T1 T2).
 
 interpretation "positive abbreviation (term)"
    'SnAbbrPos T1 T2 = (TPair (Bind2 true Abbr) T1 T2).
@@ -76,7 +76,7 @@ interpretation "negative abbreviation (term)"
    'SnAbbrNeg T1 T2 = (TPair (Bind2 false Abbr) T1 T2).
 
 interpretation "abstraction (term)"
-   'SnAbst a T1 T2 = (TPair (Bind2 a Abst) T1 T2).
+   'SnAbst p T1 T2 = (TPair (Bind2 p Abst) T1 T2).
 
 interpretation "positive abstraction (term)"
    'SnAbstPos T1 T2 = (TPair (Bind2 true Abst) T1 T2).
@@ -117,7 +117,7 @@ fact destruct_tpair_tpair_aux: ∀I1,I2,T1,T2,V1,V2. ②{I1}T1.V1 = ②{I2}T2.V2
 #I1 #I2 #T1 #T2 #V1 #V2 #H destruct /2 width=1 by and3_intro/
 qed-.
 
-lemma discr_tpair_xy_x: ∀I,T,V. ②{I} V. T = V → ⊥.
+lemma discr_tpair_xy_x: ∀I,T,V. ②{I}V.T = V → ⊥.
 #I #T #V elim V -V
 [ #J #H destruct
 | #J #W #U #IHW #_ #H elim (destruct_tpair_tpair_aux … H) -H /2 width=1 by/ (**) (* destruct lemma needed *)
@@ -125,7 +125,7 @@ lemma discr_tpair_xy_x: ∀I,T,V. ②{I} V. T = V → ⊥.
 qed-.
 
 (* Basic_1: was: thead_x_y_y *)
-lemma discr_tpair_xy_y: ∀I,V,T. ②{I} V. T = T → ⊥.
+lemma discr_tpair_xy_y: ∀I,V,T. ②{I}V.T = T → ⊥.
 #I #V #T elim T -T
 [ #J #H destruct
 | #J #W #U #_ #IHU #H elim (destruct_tpair_tpair_aux … H) -H /2 width=1 by/ (**) (* destruct lemma needed *)
@@ -133,7 +133,7 @@ lemma discr_tpair_xy_y: ∀I,V,T. ②{I} V. T = T → ⊥.
 qed-.
 
 lemma eq_false_inv_tpair_sn: ∀I,V1,T1,V2,T2.
-                             (②{I} V1. T1 = ②{I} V2. T2 → ⊥) →
+                             (②{I}V1.T1 = ②{I}V2.T2 → ⊥) →
                              (V1 = V2 → ⊥) ∨ (V1 = V2 ∧ (T1 = T2 → ⊥)).
 #I #V1 #T1 #V2 #T2 #H
 elim (eq_term_dec V1 V2) /3 width=1 by or_introl/ #HV12 destruct
@@ -141,7 +141,7 @@ elim (eq_term_dec V1 V2) /3 width=1 by or_introl/ #HV12 destruct
 qed-.
 
 lemma eq_false_inv_tpair_dx: ∀I,V1,T1,V2,T2.
-                             (②{I} V1. T1 = ②{I} V2. T2 → ⊥) →
+                             (②{I} V1. T1 = ②{I}V2.T2 → ⊥) →
                              (T1 = T2 → ⊥) ∨ (T1 = T2 ∧ (V1 = V2 → ⊥)).
 #I #V1 #T1 #V2 #T2 #H
 elim (eq_term_dec T1 T2) /3 width=1 by or_introl/ #HT12 destruct
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_simple.ma
index 6bffbf4fa..6332ff149 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/term_simple.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/term_simple.ma
@@ -26,17 +26,17 @@ interpretation "simple (term)" 'Simple T = (simple T).
 
 (* Basic inversion lemmas ***************************************************)
 
-fact simple_inv_bind_aux: ∀T. 𝐒⦃T⦄ → ∀a,J,W,U. T = ⓑ{a,J} W. U → ⊥.
+fact simple_inv_bind_aux: ∀T. 𝐒⦃T⦄ → ∀p,J,W,U. T = ⓑ{p,J}W.U → ⊥.
 #T * -T
-[ #I #a #J #W #U #H destruct
+[ #I #p #J #W #U #H destruct
 | #I #V #T #a #J #W #U #H destruct
 ]
-qed.
+qed-.
 
-lemma simple_inv_bind: ∀a,I,V,T. 𝐒⦃ⓑ{a,I} V. T⦄ → ⊥.
+lemma simple_inv_bind: ∀p,I,V,T. 𝐒⦃ⓑ{p,I} V. T⦄ → ⊥.
 /2 width=7 by simple_inv_bind_aux/ qed-.
 
 lemma simple_inv_pair: ∀I,V,T.  𝐒⦃②{I}V.T⦄ → ∃J. I = Flat2 J.
-* /2 width=2 by ex_intro/ #a #I #V #T #H
-elim (simple_inv_bind … H)
+* /2 width=2 by ex_intro/
+#p #I #V #T #H elim (simple_inv_bind … H)
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts_vector.ma
index 936804ce9..e90370621 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/tsts_vector.ma
@@ -20,11 +20,10 @@ include "basic_2/grammar/tsts.ma".
 (* Advanced inversion lemmas ************************************************)
 
 (* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *)
-lemma tsts_inv_bind_applv_simple: ∀a,I,Vs,V2,T1,T2. ⒶVs.T1 ≂ ⓑ{a,I} V2. T2 →
+lemma tsts_inv_bind_applv_simple: ∀p,I,Vs,V2,T1,T2. ⒶVs.T1 ≂ ⓑ{p,I}V2.T2 →
                                   𝐒⦃T1⦄ → ⊥.
-#a #I #Vs #V2 #T1 #T2 #H
-elim (tsts_inv_pair2 … H) -H #V0 #T0
-elim Vs -Vs normalize
+#p #I #Vs #V2 #T1 #T2 #H elim (tsts_inv_pair2 … H) -H
+#V0 #T0 elim Vs -Vs normalize
 [ #H destruct #H /2 width=5 by simple_inv_bind/
 | #V #Vs #_ #H destruct
 ]
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/gref_1.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/gref_1.ma
index d22748809..c67265063 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/gref_1.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/gref_1.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( § term 90 p )"
+notation "hvbox( § term 90 l )"
  non associative with precedence 55
- for @{ 'GRef $p }.
+ for @{ 'GRef $l }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabbr_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabbr_3.ma
index 44116053b..f57a89c30 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabbr_3.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabbr_3.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⓓ { term 46 a } break term 55 T1 . break term 55 T2 )"
+notation "hvbox( ⓓ { term 46 p } break term 55 T1 . break term 55 T2 )"
  non associative with precedence 55
- for @{ 'SnAbbr $a $T1 $T2 }.
+ for @{ 'SnAbbr $p $T1 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabst_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabst_3.ma
index 8ba34495d..8622fb7a9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabst_3.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snabst_3.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⓛ { term 46 a } break term 55 T1 . break term 55 T2 )"
+notation "hvbox( ⓛ { term 46 p } break term 55 T1 . break term 55 T2 )"
  non associative with precedence 55
- for @{ 'SnAbst $a $T1 $T2 }.
+ for @{ 'SnAbst $p $T1 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snbind2_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snbind2_4.ma
index ceae73562..40804a359 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snbind2_4.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/snbind2_4.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⓑ { term 46 a , break term 46 I } break term 55 T1 . break term 55 T )"
+notation "hvbox( ⓑ { term 46 p , break term 46 I } break term 55 T1 . break term 55 T )"
  non associative with precedence 55
- for @{ 'SnBind2 $a $I $T1 $T }.
+ for @{ 'SnBind2 $p $I $T1 $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/star_1.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/star_1.ma
index 6307ed9e9..af8fa6675 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/star_1.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/constructors/star_1.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⋆ term 90 k )"
+notation "hvbox( ⋆ term 90 s )"
  non associative with precedence 55
- for @{ 'Star $k }.
+ for @{ 'Star $s }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/weight_1.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/weight_1.ma
index 31b4fe655..3cd52cc2f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/functions/weight_1.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/functions/weight_1.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ♯ { term 46 x } )"
+notation "hvbox( ♯ { term 46 X } )"
  non associative with precedence 90
- for @{ 'Weight $x }.
+ for @{ 'Weight $X }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/notation.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/notation.ma
index 0996c7cdb..575359650 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/notation.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/notation.ma
@@ -16,15 +16,15 @@
 
 notation "hvbox( ⦃G, L⦄ ⊢ break ⌘ ⦃ term 46 T ⦄ ≡ break term 46 k )"
    non associative with precedence 45
-   for @{ 'ICM $L $T $k }.
+   for @{ 'ICM $L $T $s }.
 
 notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T ÷ break term 46 A )"
    non associative with precedence 45
-   for @{ 'BinaryArity $h $L $T $A }.
+   for @{ 'BinaryArity $o $L $T $A }.
 
 notation "hvbox( h ⊢ break term 46 L1 ÷ ⫃ break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'LRSubEqB $h $L1 $L2 }.
+   for @{ 'LRSubEqB $o $L1 $L2 }.
 
 notation "hvbox( L1 ⊢ ⬌ break term 46 L2 )"
    non associative with precedence 45
@@ -36,12 +36,12 @@ notation "hvbox( L1 ⊢ ⬌* break term 46 L2 )"
 
 notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'NativeType $h $L $T1 $T2 }.
+   for @{ 'NativeType $o $L $T1 $T2 }.
 
 notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : : break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'NativeTypeAlt $h $L $T1 $T2 }.
+   for @{ 'NativeTypeAlt $o $L $T1 $T2 }.
 
 notation "hvbox( ⦃ term 46 h , break term 46 L ⦄ ⊢ break term 46 T1 : * break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'NativeTypeStar $h $L $T1 $T2 }.
+   for @{ 'NativeTypeStar $o $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_8.ma
index 80e40a157..a555a5f60 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_8.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpred_8.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≽ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≽ break [ term 46 o, break term 46 h ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
    non associative with precedence 45
-   for @{ 'BTPRed $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
+   for @{ 'BTPRed $o $h $G1 $L1 $T1 $G2 $L2 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredalt_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredalt_8.ma
index c3f111a0e..0b7e9ea0b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredalt_8.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredalt_8.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≽ ≽ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≽ ≽ break [ term 46 o, break term 46 h ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
    non associative with precedence 45
-   for @{ 'BTPRedAlt $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
+   for @{ 'BTPRedAlt $o $h $G1 $L1 $T1 $G2 $L2 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_8.ma
index bb6d3d1af..d155e84bd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_8.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredproper_8.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≻ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≻ break [ term 46 o, break term 46 h ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
    non associative with precedence 45
-   for @{ 'BTPRedProper $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
+   for @{ 'BTPRedProper $o $h $G1 $L1 $T1 $G2 $L2 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_8.ma
index 3943a33fd..c14e163d2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_8.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstar_8.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ break [ term 46 o, break term 46 h ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
    non associative with precedence 45
-   for @{ 'BTPRedStar $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
+   for @{ 'BTPRedStar $o $h $G1 $L1 $T1 $G2 $L2 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstaralt_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstaralt_8.ma
index 227a666f2..67609ec75 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstaralt_8.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstaralt_8.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ ≥ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≥ ≥ break [ term 46 o, break term 46 h ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
    non associative with precedence 45
-   for @{ 'BTPRedStarAlt $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
+   for @{ 'BTPRedStarAlt $o $h $G1 $L1 $T1 $G2 $L2 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma
index 207ba13bf..adacfe0a5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦥ [ term 46 h, break term 46 g ] break ⦃ term 46 G, break term 46 L, break term 46 T ⦄ )"
+notation "hvbox( ⦥ [ term 46 o, break term 46 h ] break ⦃ term 46 G, break term 46 L, break term 46 T ⦄ )"
    non associative with precedence 45
-   for @{ 'BTSN $h $g $G $L $T }.
+   for @{ 'BTSN $o $h $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma
index 7c6d69120..5e8fd5d84 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦥ ⦥ [ term 46 h, break term 46 g ] break ⦃ term 46 G, break term 46 L, break term 46 T ⦄ )"
+notation "hvbox( ⦥ ⦥ [ term 46 o, break term 46 h ] break ⦃ term 46 G, break term 46 L, break term 46 T ⦄ )"
    non associative with precedence 45
-   for @{ 'BTSNAlt $h $g $G $L $T }.
+   for @{ 'BTSNAlt $o $h $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma
index be4f9a4a9..5ac085cdc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/cosn_5.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( G ⊢ ~ ⬊ * break [ term 46 h , break term 46 g , break term 46 l ] break term 46 L )"
+notation "hvbox( G ⊢ ~ ⬊ * break [ term 46 o , break term 46 h , break term 46 f ] break term 46 L )"
    non associative with precedence 45
-   for @{ 'CoSN $h $g $l $G $L }.
+   for @{ 'CoSN $o $h $f $G $L }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/degree_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/degree_6.ma
index 7602a6544..1de815516 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/degree_6.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/degree_6.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ▪ break [ term 46 h , break term 46 g ] break term 46 d )"
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ▪ break [ term 46 o , break term 46 h ] break term 46 d )"
    non associative with precedence 45
-   for @{ 'Degree $h $g $G $L $T $d }.
+   for @{ 'Degree $o $h $G $L $T $d }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_8.ma
index 9aa3568af..433923fea 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_8.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpconvstar_8.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ⬌ * break [ term 46 h , break term 46 g , break term 46 n1 , break term 46 n2 ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ⬌ * break [ term 46 o , break term 46 h , break term 46 n1 , break term 46 n2 ] break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'DPConvStar $h $g $n1 $n2 $G $L $T1 $T2 }.
+   for @{ 'DPConvStar $o $h $n1 $n2 $G $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_7.ma
index c5f55aed8..ceb7aaf65 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_7.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/dpredstar_7.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * break [ term 46 h , break term 46 g , break term 46 n ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 • * ➡ * break [ term 46 o , break term 46 h , break term 46 n ] break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'DPRedStar $h $g $n $G $L $T1 $T2 }.
+   for @{ 'DPRedStar $o $h $n $G $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_4.ma
deleted file mode 100644
index e46480639..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/freestar_4.ma
+++ /dev/null
@@ -1,19 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
-
-notation "hvbox( L ⊢ break term 46 i ϵ 𝐅 * [ break term 46 l ] ⦃ break term 46 T ⦄ )"
-   non associative with precedence 45
-   for @{ 'FreeStar $L $i $l $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma
index e56e02e46..a2a86fddd 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazybtpredstarproper_8.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ >≡ break [ term 46 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ >≡ break [ term 46 o, break term 46 h ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
    non associative with precedence 45
-   for @{ 'LazyBTPRedStarProper $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.
+   for @{ 'LazyBTPRedStarProper $o $h $G1 $L1 $T1 $G2 $L2 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma
index a6b02b3cc..0cd902ba8 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( L1 ≡ break [ term 46 T , break term 46 l ] break term 46 L2 )"
+notation "hvbox( L1 ≡ break [ term 46 T , break term 46 f ] break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'LazyEq $T $l $L1 $L2 }.
+   for @{ 'LazyEq $T $f $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_7.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_7.ma
index 79a79e2c0..2c8f79cb3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_7.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_7.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≡ break [ term 46 l ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ≡ break [ term 46 f ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
    non associative with precedence 45
-   for @{ 'LazyEq $l $G1 $L1 $T1 $G2 $L2 $T2 }.
+   for @{ 'LazyEq $f $G1 $L1 $T1 $G2 $L2 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyor_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyor_5.ma
index 6479c1f71..70d3a1c66 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyor_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyor_5.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( L1 ⋓ break [ term 46 T , break term 46 l ] break term 46 L2 ≡ break term 46 L )"
+notation "hvbox( L1 ⋓ break [ term 46 T , break term 46 f ] break term 46 L2 ≡ break term 46 L )"
    non associative with precedence 45
-   for @{ 'LazyOr $L1 $T $l $L2 $L }.
+   for @{ 'LazyOr $L1 $T $f $L2 $L }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_4.ma
index 994e6b22b..6135be4d4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_4.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeq_4.ma
@@ -16,4 +16,4 @@
 
 notation "hvbox( L1 break ⊆ [ term 46 l , break term 46 m ] break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'LRSubEq $L1 $l $m $L2 }.
+   for @{ 'LRSubEq $L1 $l $k $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqd_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqd_5.ma
index d90e35183..b43c8bf17 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqd_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqd_5.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( G ⊢ break term 46 L1 ⫃ ▪ break [ term 46 h, break term 46 g ] break term 46 L2 )"
+notation "hvbox( G ⊢ break term 46 L1 ⫃ ▪ break [ term 46 o, break term 46 h ] break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'LRSubEqD $h $g $G $L1 $L2 }.
+   for @{ 'LRSubEqD $o $h $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma
index f6595e14d..55067b57e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lrsubeqv_5.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( G ⊢ break term 46 L1 ⫃ ¡ break [ term 46 h, break term 46 g ] break term 46 L2 )"
+notation "hvbox( G ⊢ break term 46 L1 ⫃ ¡ break [ term 46 o, break term 46 h ] break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'LRSubEqV $h $g $G $L1 $L2 }.
+   for @{ 'LRSubEqV $o $h $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/midiso_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/midiso_4.ma
index dc380d849..20297e517 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/midiso_4.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/midiso_4.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( L1 ⩬ break [ term 46 l , break term 46 m ] break term 46 L2 )"
+notation "hvbox( L1 ⩬ break [ term 46 f , break term 46 m ] break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'MidIso $l $m $L1 $L2 }.
+   for @{ 'MidIso $f $k $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_5.ma
index d6426f6c1..631034964 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_5.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ¡ break [ term 46 h, break term 46 g ] )"
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ¡ break [ term 46 o, break term 46 h ] )"
    non associative with precedence 45
-   for @{ 'NativeValid $h $g $G $L $T }.
+   for @{ 'NativeValid $o $h $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma
index 449fe1452..f2a9b70ed 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/nativevalid_6.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ¡ break [ term 46 h , break term 46 g , break term 46 d ] )"
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T ¡ break [ term 46 o , break term 46 h , break term 46 d ] )"
    non associative with precedence 45
-   for @{ 'NativeValid $h $g $d $G $L $T }.
+   for @{ 'NativeValid $o $h $d $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_6.ma
index 1a423e465..536568f7c 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_6.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/pred_6.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ break [ term 46 h , break term 46 g ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ break [ term 46 o , break term 46 h ] break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'PRed $h $g $G $L $T1 $T2 }.
+   for @{ 'PRed $o $h $G $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_6.ma
index 8360d142a..cd474d498 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_6.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_6.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 h , break term 46 g ] break 𝐍 ⦃ term 46 T2 ⦄ )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 o , break term 46 h ] break 𝐍 ⦃ term 46 T2 ⦄ )"
    non associative with precedence 45
-   for @{ 'PRedEval $h $g $G $L $T1 $T2 }.
+   for @{ 'PRedEval $o $h $G $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_5.ma
index d1e001d85..8eda91490 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednormal_5.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] 𝐍 break ⦃ term 46 T ⦄ )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ➡ break [ term 46 o , break term 46 h ] 𝐍 break ⦃ term 46 T ⦄ )"
    non associative with precedence 45
-   for @{ 'PRedNormal $h $g $G $L $T }.
+   for @{ 'PRedNormal $o $h $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednotreducible_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednotreducible_5.ma
index cb33d31e2..788e2b428 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednotreducible_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/prednotreducible_5.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] 𝐈 break ⦃ term 46 T ⦄ )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ➡ break [ term 46 o , break term 46 h ] 𝐈 break ⦃ term 46 T ⦄ )"
    non associative with precedence 45
-   for @{ 'PRedNotReducible $h $g $G $L $T }.
+   for @{ 'PRedNotReducible $o $h $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predreducible_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predreducible_5.ma
index 82ded9c03..af010f4fb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predreducible_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predreducible_5.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] 𝐑 break ⦃ term 46 T ⦄ )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ➡ break [ term 46 o , break term 46 h ] 𝐑 break ⦃ term 46 T ⦄ )"
    non associative with precedence 45
-   for @{ 'PRedReducible $h $g $G $L $T }.
+   for @{ 'PRedReducible $o $h $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma
index 206566071..86fd19efb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsn_5.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 h , break term 46 g ] break term 46 L2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ break [ term 46 o , break term 46 h ] break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'PRedSn $h $g $G $L1 $L2 }.
+   for @{ 'PRedSn $o $h $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma
index aef4f2707..f7b69c931 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ * break [ term 46 h , break term 46 g ] break term 46 L2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ * break [ term 46 o , break term 46 h ] break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'PRedSnStar $h $g $G $L1 $L2 }.
+   for @{ 'PRedSnStar $o $h $G $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_6.ma
index 54ac66647..7991322a3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_6.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predstar_6.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 h , break term 46 g ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ break term 46 T1 ➡ * break [ term 46 o , break term 46 h ] break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'PRedStar $h $g $G $L $T1 $T2 }.
+   for @{ 'PRedStar $o $h $G $L $T1 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubst_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubst_6.ma
index e35f7ca23..56cb72ec4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubst_6.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubst_6.ma
@@ -16,4 +16,4 @@
 
 notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 break ▶ [ term 46 l , break term 46 m ] break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'PSubst $G $L $T1 $l $m $T2 }.
+   for @{ 'PSubst $G $L $T1 $l $k $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststar_6.ma
index 2dd1f2d6e..90362edb6 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststar_6.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststar_6.ma
@@ -16,4 +16,4 @@
 
 notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 break ▶ * [ term 46 l , break term 46 m ] break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'PSubstStar $G $L $T1 $l $m $T2 }.
+   for @{ 'PSubstStar $G $L $T1 $l $k $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststaralt_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststaralt_6.ma
index 97227dccf..80a29a841 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststaralt_6.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststaralt_6.ma
@@ -16,4 +16,4 @@
 
 notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 break ▶ ▶ * [ term 46 l , break term 46 m ] break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'PSubstStarAlt $G $L $T1 $l $m $T2 }.
+   for @{ 'PSubstStarAlt $G $L $T1 $l $k $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_4.ma
index 291de4c0e..be5936abf 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_4.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rdropstar_4.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⬇ * [ term 46 s , break term 46 m ] break term 46 L1 ≡ break term 46 L2 )"
+notation "hvbox( ⬇ * [ term 46 c , break term 46 f ] break term 46 L1 ≡ break term 46 L2 )"
    non associative with precedence 45
-   for @{ 'RDropStar $s $m $L1 $L2 }.
+   for @{ 'RDropStar $c $f $L1 $L2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rliftstar_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rliftstar_3.ma
index af4de47ba..fa19e933e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rliftstar_3.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/rliftstar_3.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⬆ * [ term 46 m ] break term 46 T1 ≡ break term 46 T2 )"
+notation "hvbox( ⬆ * [ term 46 f ] break term 46 T1 ≡ break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'RLiftStar $m $T1 $T2 }.
+   for @{ 'RLiftStar $f $T1 $T2 }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_5.ma
index bfc7d0cb0..ac83d2797 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_5.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬊ * break [ term 46 h , break term 46 g ] break term 46 T )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬊ * break [ term 46 o, break term 46 h ] break term 46 T )"
    non associative with precedence 45
-   for @{ 'SN $h $g $G $L $T }.
+   for @{ 'SN $o $h $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma
index c402cdc8a..00db2bfe0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/sn_6.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( G ⊢ ⬊ * break [ term 46 h , break term 46 g , break term 46 T , break term 46 l ] break term 46 L )"
+notation "hvbox( G ⊢ ⬊ * break [ term 46 o , break term 46 h , break term 46 T , break term 46 f ] break term 46 L )"
    non associative with precedence 45
-   for @{ 'SN $h $g $T $l $G $L }.
+   for @{ 'SN $o $h $T $f $G $L }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_5.ma
index 13fed06c7..c64d194e3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_5.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_5.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬊ ⬊ * break [ term 46 h , break term 46 g ] break term 46 T )"
+notation "hvbox( ⦃ term 46 G, break term 46 L ⦄ ⊢ ⬊ ⬊ * break [ term 46 o , break term 46 h ] break term 46 T )"
    non associative with precedence 45
-   for @{ 'SNAlt $h $g $G $L $T }.
+   for @{ 'SNAlt $o $h $G $L $T }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma
index 4beb9fdcf..251ae4158 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/snalt_6.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( G ⊢ ⬊ ⬊ * break [ term 46 h , break term 46 g , break term 46 T , break term 46 l ] break term 46 L )"
+notation "hvbox( G ⊢ ⬊ ⬊ * break [ term 46 o , break term 46 h , break term 46 T , break term 46 f ] break term 46 L )"
    non associative with precedence 45
-   for @{ 'SNAlt $h $g $T $l $G $L }.
+   for @{ 'SNAlt $o $h $T $f $G $L }.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestar_6.ma
index b7d6a71e0..369838563 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestar_6.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/statictypestar_6.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************)
 
-notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 •* break [ term 46 h , break term 46 n ] break term 46 T2 )"
+notation "hvbox( ⦃ term 46 G , break term 46 L ⦄ ⊢ break term 46 T1 •* break [ term 46 o , break term 46 n ] break term 46 T2 )"
    non associative with precedence 45
-   for @{ 'StaticTypeStar $h $G $L $n $T1 $T2 }.
+   for @{ 'StaticTypeStar $o $G $L $n $T1 $T2 }.