From 0733a61e7b3a0f6173b403e3bfc2257b725b44f2 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 27 Jan 2014 22:06:00 +0000
Subject: [PATCH] some corrections ...

---
 .../basic_2/computation/cpxs_cpys.ma          | 25 ++++++-----
 .../basic_2/computation/cpxs_lleq.ma          |  4 ++
 .../basic_2/computation/csx_tstc_vector.ma    |  2 +-
 .../basic_2/computation/lpxs_lleq.ma          | 32 +++++++++++++
 .../basic_2/computation/lsx_csx.ma            | 45 +++++++++++++++++--
 .../lambdadelta/basic_2/reduction/cnx.ma      |  2 +-
 .../lambdadelta/basic_2/reduction/cpx_lleq.ma |  4 ++
 .../lambdadelta/basic_2/relocation/cpy.ma     | 14 ++++++
 .../lambdadelta/basic_2/relocation/cpy_cpy.ma |  3 ++
 .../basic_2/relocation/cpy_lift.ma            |  4 ++
 .../basic_2/relocation/lift_lift.ma           |  2 +-
 matita/matita/predefined_virtuals.ml          |  1 +
 12 files changed, 121 insertions(+), 17 deletions(-)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma
index 7ab36e5be..2b4eadd6e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma
@@ -30,9 +30,8 @@ lemma cpys_tpxs_trans: ∀h,g,G,L,T1,T,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T →
 /3 width=5 by cpxs_strap1, cpys_cpx, lsubr_cpx_trans, cpx_cpxs/
 qed-.
 
-axiom cpx_fwd_cpys_tpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
+lemma cpx_fwd_cpys_tpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
                          ∃∃T. ⦃G, L⦄ ⊢ T1 ▶*×[0, ∞] T & ⦃G, ⋆⦄ ⊢ T ➡*[h, g] T2.
-(*
 #h #g #G #L #T1 #T2 #H elim H -G -L -T1 -T2
 [ /2 width=3 by ex2_intro/
 | /4 width=3 by cpx_cpxs, cpx_sort, ex2_intro/
@@ -41,12 +40,18 @@ axiom cpx_fwd_cpys_tpxs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 →
   lapply (cpxs_lift … HV2 (⋆) (Ⓣ) … HVW … HVW2)
   [ @ldrop_atom #H destruct | /3 width=7 by cpys_subst_Y2, ex2_intro/ ]
 | #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ * #V #HV1 #HV2 * #T #HT1 #HT2
-  elim (cpys_split_down … HT1 1) -HT1 // #T0 #HT10 #HT0 
-(*  
-  @(ex2_intro … (ⓑ{a,I}V.T0))
-  [ @cpys_bind // 
-  | @(cpxs_bind … HV2) -HV2
+  @(ex2_intro … (ⓑ{a,I}V1.T))
+  [ @cpys_bind //
+  | @cpxs_bind //
   
-  /2 width=5 by cpys_tpxs_trans/
-  ]
-*)*)
\ No newline at end of file
+  elim (cpys_split_down … HT1 1) -HT1 // #T0 #HT10 #HT0
+  @(ex2_intro … (ⓑ{a,I}V.T0))
+  [ @cpys_bind //
+  | @(cpxs_trans … (ⓑ{a,I}V.T)) @cpxs_bind // -HT10
+
+
+(*  
+  lapply (lsuby_cpys_trans … HT10 (L.ⓑ{I}V) ?) -HT10 /2 width=1 by lsuby_succ/ #HT10
+*)
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ * #V #HV1 #HV2 *
+  /3 width=5 by cpys_flat, cpxs_flat, ex2_intro/
\ No newline at end of file
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma
index 6c5b811eb..7a5666593 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma
@@ -29,3 +29,7 @@ lemma lleq_cpxs_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[h, g] T2 →
                          ∀L1. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2.
 #h #g #G #L2 #T1 #T2 #H @(cpxs_ind … H) -T2 /3 width=6 by lleq_cpx_conf_dx/
 qed-.
+
+lemma lleq_cpxs_conf_sn: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 →
+                         ∀L2. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2.
+/4 width=6 by lleq_cpxs_conf_dx, lleq_sym/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
index 55099d325..21431dc3b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
@@ -35,7 +35,7 @@ qed.
 
 lemma csx_applv_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k.
 #h #g #G #L #k elim (deg_total h g k)
-#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=1 by csx_applv_cnx, cnx_sort, simple_atom/ ]
+#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ ]
 #l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl
 #Hkl #Vs elim Vs -Vs /2 width=1 by/
 #V #Vs #IHVs #HVVs
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma
index a919045df..730604ddb 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma
@@ -20,6 +20,38 @@ include "basic_2/computation/lpxs_cpxs.ma".
 
 (* Advanced properties ******************************************************)
 
+fact le_repl_sn_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z.
+// qed-.
+
+fact pippo_aux: ∀h,g,G,L1,T,T1,d,e. ⦃G, L1⦄ ⊢ T ▶×[d, e] T1 → e = ∞ →
+                ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
+                ∃∃T2. ⦃G, L2⦄ ⊢ T ▶×[d, e] T2 & ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 &
+                      L1 ⋕[T, d] L2 ↔ T1 = T2.
+#h #g #G #L1 #T #T1 #d #e #H elim H -G -L1 -T -T1 -d -e [ * ]
+[ /5 width=5 by lpxs_fwd_length, lleq_sort, ex3_intro, conj/
+| #i #G #L1 elim (lt_or_ge i (|L1|)) [2: /6 width=6 by lpxs_fwd_length, lleq_free, le_repl_sn_aux, ex3_intro, conj/ ]
+  #Hi #d elim (ylt_split i d) [ /5 width=5 by lpxs_fwd_length, lleq_skip, ex3_intro, conj/ ]
+  #Hdi #e #He #L2 elim (lleq_dec (#i) L1 L2 d) [ /4 width=5 by lpxs_fwd_length, ex3_intro, conj/ ]
+  #HnL12 #HL12 elim (ldrop_O1_lt L1 i) // -Hi #I #K1 #V1 #HLK1
+  elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+  elim (lpxs_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+  elim (lift_total V2 0 (i+1)) #W2 #HVW2
+  @(ex3_intro … W2) /2 width=7 by cpxs_delta, cpy_subst/ -I -K1 -V1 -Hdi
+  @conj #H [ elim HnL12 // | destruct elim (lift_inv_lref2_be … HVW2) // ]
+| /5 width=5 by lpxs_fwd_length, lleq_gref, ex3_intro, conj/
+| #I #G #L1 #K1 #V1 #W1 #i #d #e #Hdi #Hide #HLK1 #HVW1 #He #L2 #HL12 destruct
+  elim (lpxs_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
+  elim (lpxs_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct
+  lapply (ldrop_fwd_drop2 … HLK1) -HLK1 #HLK1
+  elim (lift_total V2 0 (i+1)) #W2 #HVW2
+  @(ex3_intro … W2) /2 width=10 by cpxs_lift, cpy_subst/
+  
+  
+  elim (lleq_dec (#i) L1 L2 d) 
+    
+|
+]  
+
 axiom lleq_lpxs_trans: ∀h,g,G,L1,L2,T,d. L1 ⋕[T, d] L2 → ∀K2. ⦃G, L2⦄ ⊢ ➡*[h, g] K2 →
                        ∃∃K1. ⦃G, L1⦄ ⊢ ➡*[h, g] K1 & K1 ⋕[T, d] K2.
 (*
diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma
index 670fb9473..883e32d0b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_csx.ma
@@ -19,7 +19,44 @@ include "basic_2/computation/lsx_lpxs.ma".
 (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************)
 
 (* Advanced forward lemmas **************************************************)
+
+include "basic_2/computation/cpxs_lleq.ma".
+
 (*
+lemma lsx_cpxs_conf: ∀h,g,G,L1,T1,T2. G ⊢ ⋕⬊*[h, g, T1] L1 →
+                     ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 →
+                     G ⊢ ⋕⬊*[h, g, T2] L2.
+#h #g #G #L1 #T1 #T2 #H @(lsx_ind … H) -L1
+#L1 #HL1 #IHL1 #L2 #HL12 #HT12 @lsx_intro
+#L3 #HL23 #HnL23 elim (lleq_dec T2 L1 L2 0) [| -HnL23 ]
+[ #HT2 @(IHL1 L3) /2 width=3 by lpxs_trans/
+
+ @(lsx_lpxs_trans … HL23) 
+| #HnT2 @(lsx_lpxs_trans … HL23) @(IHL1 … L2) //
+  #HT1 @HnT2 @(lleq_cpxs_conf_dx … HT12) //
+]
+*)
+
+lemma lsx_fwd_bind_dx_lpxs: ∀h,g,a,I,G,L1,V1. ⦃G, L1⦄ ⊢ ⬊*[h, g] V1 →
+                            ∀L2,T. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V1.T] L2 → 
+                            ∀V2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → ⦃G, L2⦄ ⊢ V1 ➡*[h, g] V2 →
+                            G ⊢ ⋕⬊*[h, g, T] L2.ⓑ{I}V2.
+#h #g #a #I #G #L1 #V1 #H @(csx_ind_alt … H) -V1
+#V1 #_ #IHV1 #L2 #T #H @(lsx_ind … H) -L2
+#L2 #HL2 #IHL2 #V2 #HL12 #HV12 @lsx_intro
+#Y #H #HnT elim (lpxs_inv_pair1 … H) -H
+#L3 #V3 #HL23 #HV23 #H destruct
+lapply (lpxs_trans … HL12 … HL23) #HL13
+elim (eq_term_dec V2 V3)
+[ (* -HV13 -HL2 -IHV1 -HL12 *) #H destruct
+  @IHL2 -IHL2 // -HL23 -HL13 /3 width=2 by lleq_fwd_bind_O/
+| -IHL2 -HnT #HnV23 elim (eq_term_dec V1 V2)
+  [ #H -HV12 destruct
+  (*  @(lsx_lpxs_trans … (L2.ⓑ{I}V2)) /2 width=1 by lpxs_pair/ *)
+    @(IHV1 … HnV23) -IHV1 -HnV23 /2 width=3 by lpxs_cpxs_trans/ -HL12 -HL13
+  @(lsx_lpxs_trans … HL23)
+
+
 lemma lsx_fwd_bind_dx_lpxs: ∀h,g,a,I,G,L1,V. ⦃G, L1⦄ ⊢ ⬊*[h, g] V →
                             ∀L2,T. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T] L2 → ⦃G, L1⦄ ⊢ ➡*[h, g] L2 →
                             G ⊢ ⋕⬊*[h, g, T] L2.ⓑ{I}V.
@@ -32,10 +69,10 @@ lapply (lpxs_trans … HL12 … HL23) #HL13
 elim (eq_term_dec V1 V3)
 [ -HV13 -HL2 -IHV1 -HL12 #H destruct
   @IHL2 -IHL2 // -HL23 -HL13 /3 width=2 by lleq_fwd_bind_O/
-| -IHL2 -HL23 -HnT #HnV13
-  @(IHV1 … HnV13) -IHV1 -HnV13 /2 width=3 by lpxs_cpxs_trans/ -HL12 -HL13 -HV13
-  @(lsx_lpxs_trans) … HL2)
-*)
+| -IHL2 -HnT #HnV13
+  @(IHV1 … HnV13) -IHV1 -HnV13 /2 width=3 by lpxs_cpxs_trans/ -HL12 -HL13
+  @(lsx_lpxs_trans … HL23)
+
 
 (* Advanced inversion lemmas ************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
index 9954e6edb..d423f119e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cnx.ma
@@ -103,7 +103,7 @@ qed.
 
 lemma cnx_sort_iter: ∀h,g,G,L,k,l. deg h g k l → ⦃G, L⦄ ⊢ 𝐍[h, g]⦃⋆((next h)^l k)⦄.
 #h #g #G #L #k #l #Hkl
-lapply (deg_iter … l Hkl) -Hkl <minus_n_n /2 width=1 by cnx_sort/
+lapply (deg_iter … l Hkl) -Hkl <minus_n_n /2 width=6 by cnx_sort/
 qed.
 
 lemma cnx_abst: ∀h,g,a,G,L,W,T. ⦃G, L⦄ ⊢ 𝐍[h, g]⦃W⦄ → ⦃G, L.ⓛW⦄ ⊢ 𝐍[h, g]⦃T⦄ →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
index d810ae175..6ff6c39d0 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
@@ -72,3 +72,7 @@ lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
   | /3 width=3 by lleq_bind_repl_O/
 ]
 qed-.
+
+lemma lleq_cpx_conf_sn: ∀h,g,G,L1,T1,T2. ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2 →
+                        ∀L2. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2.
+/4 width=6 by lleq_cpx_conf_dx, lleq_sym/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
index 829fea318..0e440cf7f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
@@ -53,6 +53,7 @@ lemma cpy_refl: ∀G,T,L,d,e. ⦃G, L⦄ ⊢ T ▶×[d, e] T.
 #G #T elim T -T // * /2 width=1 by cpy_bind, cpy_flat/
 qed.
 
+(* Basic_1: was: subst1_ex *)
 lemma cpy_full: ∀I,G,K,V,T1,L,d. ⇩[d] L ≡ K.ⓑ{I}V →
                 ∃∃T2,T. ⦃G, L⦄ ⊢ T1 ▶×[d, 1] T2 & ⇧[d, 1] T ≡ T2.
 #I #G #K #V #T1 elim T1 -T1
@@ -205,12 +206,14 @@ lemma cpy_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶×[d, e] T2 →
                                 I = LRef i.
 /2 width=4 by cpy_inv_atom1_aux/ qed-.
 
+(* Basic_1: was: subst1_gen_sort *)
 lemma cpy_inv_sort1: ∀G,L,T2,k,d,e. ⦃G, L⦄ ⊢ ⋆k ▶×[d, e] T2 → T2 = ⋆k.
 #G #L #T2 #k #d #e #H
 elim (cpy_inv_atom1 … H) -H //
 * #I #K #V #i #_ #_ #_ #_ #H destruct
 qed-.
 
+(* Basic_1: was: subst1_gen_lref *)
 lemma cpy_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶×[d, e] T2 →
                      T2 = #i ∨
                      ∃∃I,K,V. d ≤ i & i < d + e &
@@ -279,6 +282,7 @@ qed-.
 lemma cpy_inv_refl_O2: ∀G,L,T1,T2,d. ⦃G, L⦄ ⊢ T1 ▶×[d, 0] T2 → T1 = T2.
 /2 width=6 by cpy_inv_refl_O2_aux/ qed-.
 
+(* Basic_1: was: subst1_gen_lift_eq *)
 lemma cpy_inv_lift1_eq: ∀G,T1,U1,d,e. ⇧[d, e] T1 ≡ U1 →
                         ∀L,U2. ⦃G, L⦄ ⊢ U1 ▶×[d, e] U2 → U1 = U2.
 #G #T1 #U1 #d #e #HTU1 #L #U2 #HU12 elim (cpy_up … HU12 … HTU1) -HU12 -HTU1
@@ -307,3 +311,13 @@ lemma cpy_fwd_shift1: ∀G,L1,L,T1,T,d,e. ⦃G, L⦄ ⊢ L1 @@ T1 ▶×[d, e] T
   /2 width=3 by trans_eq/
 ]
 qed-.
+
+(* Basic_1: removed theorems 25:
+            subst0_gen_sort subst0_gen_lref subst0_gen_head subst0_gen_lift_lt
+            subst0_gen_lift_false subst0_gen_lift_ge subst0_refl subst0_trans
+            subst0_lift_lt subst0_lift_ge subst0_lift_ge_S subst0_lift_ge_s
+            subst0_subst0 subst0_subst0_back subst0_weight_le subst0_weight_lt
+            subst0_confluence_neq subst0_confluence_eq subst0_tlt_head
+            subst0_confluence_lift subst0_tlt
+            subst1_head subst1_gen_head subst1_lift_S subst1_confluence_lift
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma
index a601a989e..055fe055d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma
@@ -18,6 +18,7 @@ include "basic_2/relocation/cpy_lift.ma".
 
 (* Main properties **********************************************************)
 
+(* Basic_1: was: subst1_confluence_eq *)
 theorem cpy_conf_eq: ∀G,L,T0,T1,d1,e1. ⦃G, L⦄ ⊢ T0 ▶×[d1, e1] T1 →
                      ∀T2,d2,e2. ⦃G, L⦄ ⊢ T0 ▶×[d2, e2] T2 →
                      ∃∃T. ⦃G, L⦄ ⊢ T1 ▶×[d2, e2] T & ⦃G, L⦄ ⊢ T2 ▶×[d1, e1] T.
@@ -44,6 +45,7 @@ theorem cpy_conf_eq: ∀G,L,T0,T1,d1,e1. ⦃G, L⦄ ⊢ T0 ▶×[d1, e1] T1 →
 ]
 qed-.
 
+(* Basic_1: was: subst1_confluence_neq *)
 theorem cpy_conf_neq: ∀G,L1,T0,T1,d1,e1. ⦃G, L1⦄ ⊢ T0 ▶×[d1, e1] T1 →
                       ∀L2,T2,d2,e2. ⦃G, L2⦄ ⊢ T0 ▶×[d2, e2] T2 →
                       (d1 + e1 ≤ d2 ∨ d2 + e2 ≤ d1) →
@@ -75,6 +77,7 @@ theorem cpy_conf_neq: ∀G,L1,T0,T1,d1,e1. ⦃G, L1⦄ ⊢ T0 ▶×[d1, e1] T1 
 qed-.
 
 (* Note: the constant 1 comes from cpy_subst *)
+(* Basic_1: was: subst1_trans *)
 theorem cpy_trans_ge: ∀G,L,T1,T0,d,e. ⦃G, L⦄ ⊢ T1 ▶×[d, e] T0 →
                       ∀T2. ⦃G, L⦄ ⊢ T0 ▶×[d, 1] T2 → 1 ≤ e → ⦃G, L⦄ ⊢ T1 ▶×[d, e] T2.
 #G #L #T1 #T0 #d #e #H elim H -G -L -T1 -T0 -d -e
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma
index 8ca9622b9..715035121 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma
@@ -19,6 +19,7 @@ include "basic_2/relocation/cpy.ma".
 
 (* Properties on relocation *************************************************)
 
+(* Basic_1: was: subst1_lift_lt *)
 lemma cpy_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 →
                    ∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K →
                    ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
@@ -78,6 +79,7 @@ lemma cpy_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 →
 ]
 qed-.
 
+(* Basic_1: was: subst1_lift_ge *)
 lemma cpy_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶×[dt, et] T2 →
                    ∀L,U1,U2,s,d,e. ⇩[s, d, e] L ≡ K →
                    ⇧[d, e] T1 ≡ U1 → ⇧[d, e] T2 ≡ U2 →
@@ -105,6 +107,7 @@ qed-.
 
 (* Inversion lemmas on relocation *******************************************)
 
+(* Basic_1: was: subst1_gen_lift_lt *)
 lemma cpy_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 →
                         ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
                         dt + et ≤ d →
@@ -173,6 +176,7 @@ lemma cpy_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 
 ]
 qed-.
 
+(* Basic_1: was: subst1_gen_lift_ge *)
 lemma cpy_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶×[dt, et] U2 →
                         ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
                         yinj d + e ≤ dt →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_lift.ma
index 6aac2af44..00973b220 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lift_lift.ma
@@ -85,7 +85,7 @@ theorem lift_div_be: ∀d1,e1,T1,T. ⇧[d1, e1] T1 ≡ T →
     lapply (le_plus_to_minus … Hie1d1e2) #Hd1e21i
     elim (le_inv_plus_l … Hie1d1e2) -Hie1d1e2 #Hd1e12 #He2ie1
     @ex2_intro [2: /2 width=1/ | skip ] -Hd1e12
-    @lift_lref_ge_minus_eq [ >plus_minus_commutative // | /2 width=1/ ]
+    @lift_lref_ge_minus_eq [ >plus_minus_associative // | /2 width=1/ ]
   ]
 | #p #d1 #e1 #e #e2 #T2 #H >(lift_inv_gref2 … H) -H /2 width=3/
 | #a #I #V1 #V #T1 #T #d1 #e1 #_ #_ #IHV1 #IHT1 #e #e2 #X #H #He1 #He1e2
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 8fd858f54..42a14c179 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1503,6 +1503,7 @@ let load_predefined_virtuals () =
 ;;
 
 let predefined_classes = [
+ ["&"; "⅋"; ];  
  ["!"; "¡"; "⫯"; "⫰"; ]; 
  ["?"; "¿"; "⸮"; ];
  [":"; "⁝"; ];
-- 
2.39.2