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 (file)
index 7a0cdfc..0000000
--- 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 96dec98ba281f3402698c85d48b1f11fcb6888d0..7f44246c7bde31c709c73a12f6e770df1d76c5a6 100644 (file)
--- 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 3669ca151440c22308b55b73c06a0e6568b4ff86..fb2bcaf94cff0b3f8232069d9f7979a79f0a6acb 100644 (file)
--- 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 d7c923dd494274a4e539b21477579c2df841083d..5fb0671c284e1cd188f01368d76837352878580e 100644 (file)
--- 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 27d019994d0b475161ab9ed073d20f2338a925d7..c614e0f4e9f0752d4ed990bf43fc3f63f7842ad7 100644 (file)
--- 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 cb69d3687b3476b60b390b8711f536a59763a442..ab861be57187a8405c5fcad6e59ff7cecf6112f2 100644 (file)
--- 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 (file)
index 0000000..29fee0e
--- /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 e70058dc9f3be994f09fecc19e75e1e1b8e37a29..ff00f4f84c45721632cac4321209c24f8de38347 100644 (file)
--- 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 6bffbf4fa751fb659aa5bff3ddab1c23ba8ee037..6332ff149a2f94db65cc42751394393df1aea055 100644 (file)
--- 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 936804ce9292176499c0f773aed31402ff38df00..e903706213be32b6e38fd089b4b8864819e02a33 100644 (file)
--- 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 d22748809cd55026dcc5eab3b21f6b9cd46c3ff5..c672650632d5844ea4697c51d5e77fa4fe037c9f 100644 (file)
--- 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 44116053b2aa52883efd7f061db15d0bffb3cf24..f57a89c30b598e2cae8f12edbfad06fc680f0aeb 100644 (file)
--- 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 8ba34495d21ba845dffb6b4b21a503f0043978d0..8622fb7a971312241e2a34ddd35ba8f493bf0377 100644 (file)
--- 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 ceae73562dfd1a329fd91894e56fc239ead6905b..40804a3597e80ee411aa5febc26d16db69d8fee8 100644 (file)
--- 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 6307ed9e97c192f77b83b4ce5f4636b90ebaea0b..af8fa6675073e83bd067de8a078258f2440021f8 100644 (file)
--- 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 31b4fe6555877fc19f91f8511b756aa2398cb5b7..3cd52cc2fe48c579499e980dfd7cf8e7d9b2c68c 100644 (file)
--- 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 0996c7cdb221fe65ca202cfdd60b5d038cc0e67f..575359650a36bee0a45d9a8449015fa94559ffb8 100644 (file)
--- 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 80e40a157484ed2226a3da7d2d7b541973c06f23..a555a5f60714c9071ab661046a03d30d0acc3ed1 100644 (file)
--- 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 c3f111a0ec3e0810a3119858819c51fa6223ca9c..0b7e9ea0b6b8491daf2794382ee0255407271bfa 100644 (file)
--- 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 bb6d3d1afb9411390ab64f356abc8198da632936..d155e84bd6454be11c700ad6d5f3a093380ee752 100644 (file)
--- 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 3943a33fd00f6e15c1ad2df0a987a8a222cd30d0..c14e163d23fd52cfe4881f1ee56a3b0f0b3c865b 100644 (file)
--- 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 227a666f261017c93d947aa9ff2bff4295acdd08..67609ec7564d33400bd0015f45c8dc2a07ea114a 100644 (file)
--- 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 207ba13bf278ab75c79776ba7f68df8a48d6e4b8..adacfe0a5576a8b276eec4f23ded0d539901aff0 100644 (file)
--- 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 7c6d691205a58229b0495b269236b328d258e71b..5e8fd5d84b52dec4eb1262dd0f8054930917f0eb 100644 (file)
--- 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 be4f9a4a9ff4b256bd67f08a44bf22c574f90f66..5ac085cdc0bac213b3743de258cf8f15a2cbe481 100644 (file)
--- 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 7602a654472e96bd12d67c860aff6a7030d3c689..1de8155166e102434ad6fa475fd23923a022e5ad 100644 (file)
--- 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 9aa3568afd302c2b36cc6f3d8260c6599a47e48a..433923fea565613f7e81aaa9484a8505f7c1afe6 100644 (file)
--- 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 c5f55aed816ea4577a09069e2531fdf1adc3a01d..ceb7aaf654dc4ca2b1779a76759b8ce8b5ff39fa 100644 (file)
--- 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 (file)
index e464806..0000000
--- 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 e56e02e465937c586f60cfe92a3e9f409ebdd4dc..a2a86fddd63cbf55a9bc072319de23a67601c907 100644 (file)
--- 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 a6b02b3cc43eb559f9bfe53fef283299b8788deb..0cd902ba84fa55a3c0612484c040398ea3e778b6 100644 (file)
--- 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 79a79e2c084e0c94051d5b4f9904d2e2b95457eb..2c8f79cb385d86a50b04698510343fb546dd8953 100644 (file)
--- 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 6479c1f71095785ecb0e5d1abeaa78493892e13f..70d3a1c66daccf119df8435daf1ddf8c7d76d54b 100644 (file)
--- 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 994e6b22bdc657f7431d468a359784d1da94062a..6135be4d41ae1ac868af73f34397a0df759d0ff5 100644 (file)
--- 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 d90e3518398b7a47aa8d229cf48f855b5aefb1a7..b43c8bf1762f4aa86cd7947ef637a2425282e4ab 100644 (file)
--- 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 f6595e14d20576de320a3b39b1659865ef706d66..55067b57e57f23bc0774a76619f0349eb02196d1 100644 (file)
--- 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 dc380d849b08a56d3a3a0770616c8ae4f2dd7b96..20297e51712471313ca25521be46619f41da28a7 100644 (file)
--- 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 d6426f6c174a5eca6fa2444dffd58906d29dc0a3..631034964e3b905302d291580f066fc0c9f975ef 100644 (file)
--- 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 449fe14529673ad63109efe30bc161e74b86cb20..f2a9b70ed11dbddfe990122af4f2e8f3cba3e6f3 100644 (file)
--- 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 1a423e465c83f131d579bddec6cc420dd445d947..536568f7c23fa4c402013455d60061927d0be7b4 100644 (file)
--- 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 8360d142a9b19c08fb03242bec3a51caebf2f329..cd474d4987f876ec68a2ad00455d5aea37fc39e7 100644 (file)
--- 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 d1e001d8521974ab538050da706a946a02c5b43e..8eda91490f142f822177f07ce7e2922e483b09fa 100644 (file)
--- 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 cb33d31e297153de594ffd23c2d5c9f545e6981b..788e2b4284203c3afa1fa6324456b39e8aa19d8a 100644 (file)
--- 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 82ded9c0345240ff9393f8e6bc658c0ca24a59ad..af010f4fb3718ac55d7fbeaa625377f8a0fc3b12 100644 (file)
--- 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 206566071d3da274821ae10507206c9af2a901d8..86fd19efbc8e071b63f785fe83ea0605d4990cd7 100644 (file)
--- 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 aef4f270752e678f92dc66729b24caec2533addb..f7b69c931c368082ebe3a89048c285117f635832 100644 (file)
--- 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 54ac6664769476d9bde69f9916fe98091ee3151c..7991322a334f921294b35a067571a13cf8aa425b 100644 (file)
--- 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 e35f7ca23a848b523cd62f3e3ca46f51a24152a1..56cb72ec480968106517665c8d0512b3d0e1254d 100644 (file)
--- 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 2dd1f2d6ef61882f4d83e5fa0ff627cc7e4ad298..90362edb6f42b06d88df2361e95102680a629456 100644 (file)
--- 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 97227dccfb001977d1b11ccf432c671fc65993bc..80a29a841bc92901dc534d4e422226c33711dc2d 100644 (file)
--- 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 291de4c0e5834ef5cc1c826bd3fc492a2175bd1d..be5936abf75339ca751da4dc7e8032572d78b9e4 100644 (file)
--- 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 af4de47ba2dfb6ddc5fe484ff268d09a9795741f..fa19e933e09d7aa2f219fc2d1f78969f11d16e9e 100644 (file)
--- 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 bfc7d0cb03cfec1cdf9cffe93845b1ea178ff9bd..ac83d2797249cf96d99b65ffb5c26e9a496aa00e 100644 (file)
--- 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 c402cdc8abe8801140dafdf344437518ea9d1d34..00db2bfe0d85800b38c9e80a771c9c3953c22a70 100644 (file)
--- 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 13fed06c70e6a543dc849d3ef5dcb17f9b2a2e1f..c64d194e39bb9232b26fb194a7572ca04c146829 100644 (file)
--- 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 4beb9fdcf9b106a08d7608988dbd76c2ba79276f..251ae415874134ded168d856e46ed8b794e3f6a3 100644 (file)
--- 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 b7d6a71e09b9890602525388ee7ada8244a758d2..3698385637f43a55fd81336041e8bd8bdc08361c 100644 (file)
--- 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 }.