From 1efc4c2c7be1e4aff0ccccabf905d45795b3865f Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 21 Apr 2012 13:20:21 +0000
Subject: [PATCH] - lambda_delta: static type assignment is defined -
 predefined_virtuals: some additions - nat: we added a lemma

---
 .../contribs/lambda_delta/basic_2/basic_1.txt |   7 -
 .../basic_2/{native => dynamic}/nta.ma        |   0
 .../basic_2/{native => dynamic}/nta_lift.ma   |  56 ++++----
 .../contribs/lambda_delta/basic_2/notation.ma |  14 +-
 .../lambda_delta/basic_2/static/sta.ma        | 128 ++++++++++++++++++
 .../lambda_delta/basic_2/static/sta_lift.ma   | 122 +++++++++++++++++
 .../lambda_delta/basic_2/static/sta_sta.ma    |  44 ++++++
 matita/matita/lib/arithmetics/nat.ma          |   3 +
 matita/matita/predefined_virtuals.ml          |   1 +
 9 files changed, 338 insertions(+), 37 deletions(-)
 rename matita/matita/contribs/lambda_delta/basic_2/{native => dynamic}/nta.ma (100%)
 rename matita/matita/contribs/lambda_delta/basic_2/{native => dynamic}/nta_lift.ma (80%)
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/sta.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/sta_lift.ma
 create mode 100644 matita/matita/contribs/lambda_delta/basic_2/static/sta_sta.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
index 92bd9860d..1b6aaa13f 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
+++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
@@ -204,13 +204,6 @@ pr3/pr1 pr3_pr1
 pr3/props pr3_eta
 pr3/subst1 pr3_gen_cabbr
 sn3/props sns3_lifts
-sty0/fwd sty0_gen_sort
-sty0/fwd sty0_gen_lref
-sty0/fwd sty0_gen_bind
-sty0/fwd sty0_gen_appl
-sty0/fwd sty0_gen_cast
-sty0/props sty0_lift
-sty0/props sty0_correct
 sty1/cnt sty1_cnt
 sty1/props sty1_trans
 sty1/props sty1_bind
diff --git a/matita/matita/contribs/lambda_delta/basic_2/native/nta.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma
similarity index 100%
rename from matita/matita/contribs/lambda_delta/basic_2/native/nta.ma
rename to matita/matita/contribs/lambda_delta/basic_2/dynamic/nta.ma
diff --git a/matita/matita/contribs/lambda_delta/basic_2/native/nta_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma
similarity index 80%
rename from matita/matita/contribs/lambda_delta/basic_2/native/nta_lift.ma
rename to matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma
index 6e9d1b2a2..a0ece8cbf 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/native/nta_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_lift.ma
@@ -13,14 +13,14 @@
 (**************************************************************************)
 
 include "basic_2/equivalence/cpcs_cpcs.ma".
-include "basic_2/native/nta.ma".
+include "basic_2/dynamic/nta.ma".
 
 (* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
 
 (* Advanced inversion lemmas ************************************************)
 
-fact nta_inv_sort_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀k0. T = ⋆k0 →
-                       L ⊢ ⋆(next h k0) ⬌* U.
+fact nta_inv_sort1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀k0. T = ⋆k0 →
+                        L ⊢ ⋆(next h k0) ⬌* U.
 #h #L #T #U #H elim H -L -T -U
 [ #L #k #k0 #H destruct //
 | #L #K #V #W #U #i #_ #_ #_ #_ #k0 #H destruct
@@ -36,16 +36,16 @@ fact nta_inv_sort_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀k0. T = ⋆k0 →
 qed.
 
 (* Basic_1: was: ty3_gen_sort *)
-lemma nta_inv_sort: ∀h,L,U,k. ⦃h, L⦄ ⊢ ⋆k : U → L ⊢ ⋆(next h k) ⬌* U.
+lemma nta_inv_sort1: ∀h,L,U,k. ⦃h, L⦄ ⊢ ⋆k : U → L ⊢ ⋆(next h k) ⬌* U.
 /2 width=3/ qed-.
 
-fact nta_inv_lref_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀j. T = #j →
-                       (∃∃K,V,W,U0. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
-                                    ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
-                       ) ∨
-                       (∃∃K,W,V,U0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
-                                    ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
-                       ).
+fact nta_inv_lref1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀j. T = #j →
+                        (∃∃K,V,W,U0. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
+                                     ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+                        ) ∨
+                        (∃∃K,W,V,U0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
+                                     ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+                        ).
 #h #L #T #U #H elim H -L -T -U
 [ #L #k #j #H destruct
 | #L #K #V #W #U #i #HLK #HVW #HWU #_ #j #H destruct /3 width=8/
@@ -61,18 +61,18 @@ fact nta_inv_lref_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀j. T = #j →
 qed.
 
 (* Basic_1: was ty3_gen_lref *)
-lemma nta_inv_lref: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i : U →
-                    (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
-                                 ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
-                    ) ∨
-                    (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
-                                 ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
-                    ).
+lemma nta_inv_lref1: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i : U →
+                     (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
+                                  ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+                     ) ∨
+                     (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
+                                  ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
+                     ).
 /2 width=3/ qed-.
 
-fact nta_inv_bind_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀J,X,Y. T = ⓑ{J}Y.X →
-                       ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
-                                L ⊢ ⓑ{J}Y.Z2 ⬌* U.
+fact nta_inv_bind1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀J,X,Y. T = ⓑ{J}Y.X →
+                        ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
+                                 L ⊢ ⓑ{J}Y.Z2 ⬌* U.
 #h #L #T #U #H elim H -L -T -U
 [ #L #k #J #X #Y #H destruct
 | #L #K #V #W #U #i #_ #_ #_ #_ #J #X #Y #H destruct
@@ -88,13 +88,13 @@ fact nta_inv_bind_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀J,X,Y. T = ⓑ{J}
 qed.
 
 (* Basic_1: was: ty3_gen_bind *)
-lemma nta_inv_bind: ∀h,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X : U →
-                    ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
-                             L ⊢ ⓑ{J}Y.Z2 ⬌* U.
+lemma nta_inv_bind1: ∀h,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X : U →
+                     ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
+                              L ⊢ ⓑ{J}Y.Z2 ⬌* U.
 /2 width=3/ qed-.                            
 
-fact nta_inv_cast_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓣY.X →
-                    ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
+fact nta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓣY.X →
+                     ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
 #h #L #T #U #H elim H -L -T -U
 [ #L #k #X #Y #H destruct
 | #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
@@ -110,7 +110,7 @@ fact nta_inv_cast_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓣY.X 
 qed.
 
 (* Basic_1: was: ty3_gen_cast *)
-lemma nta_inv_cast: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X : U →  ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
+lemma nta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X : U →  ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
 /2 width=3/ qed-.
 
 (* Properties on relocation *************************************************)
@@ -197,5 +197,5 @@ lemma nta_appl_old: ∀h,L,V,W,T,U. ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ T :
                     ⦃h, L⦄ ⊢ ⓐV.T : ⓐV.ⓛW.U.
 #h #L #V #W #T #U #HVW #HTU
 elim (nta_fwd_correct … HTU) #X #H
-elim (nta_inv_bind … H) -H #V0 #T0 #HWV0 #HUT0 #_ -X /3 width=2/
+elim (nta_inv_bind1 … H) -H #V0 #T0 #HWV0 #HUT0 #_ -X /3 width=2/
 qed.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
index 7be9b8ecb..dc4bda396 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
@@ -192,7 +192,7 @@ notation "hvbox( L ⊢ break term 90 T1 break [ d , break e ] ≡ break T2 )"
    non associative with precedence 45
    for @{ 'TSubst $L $T1 $d $e $T2 }.
 
-(* Static Typing ************************************************************)
+(* Static typing ************************************************************)
 
 notation "hvbox( L ⊢ break term 90 T ÷ break A )"
    non associative with precedence 45
@@ -202,6 +202,16 @@ notation "hvbox( T1 ÷ ⊑ break T2 )"
    non associative with precedence 45
    for @{ 'CrSubEqA $T1 $T2 }.
 
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 90 T1 • break T2 )"
+   non associative with precedence 45
+   for @{ 'StaticType $h $L $T1 $T2 }.
+
+(* Unwind *******************************************************************)
+
+notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 90 T1 •* break T2 )"
+   non associative with precedence 45
+   for @{ 'StaticTypeStar $h $L $T1 $T2 }.
+
 (* Reducibility *************************************************************)
 
 notation "hvbox( 𝐑 [ T ] )"
@@ -322,7 +332,7 @@ notation "hvbox( T1 ⊢ ⬌* break T2 )"
    non associative with precedence 45
    for @{ 'CPConvStar $T1 $T2 }.
 
-(* Native typing ************************************************************)
+(* Dynamic typing ***********************************************************)
 
 notation "hvbox( ⦃ h , break L ⦄ ⊢ break term 90 T1 : break T2 )"
    non associative with precedence 45
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sta.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sta.ma
new file mode 100644
index 000000000..93769e9f5
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/sta.ma
@@ -0,0 +1,128 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/substitution/ldrop.ma".
+include "basic_2/static/sh.ma".
+
+(* STATIC TYPE ASSIGNMENT ON TERMS ******************************************)
+
+inductive sta (h:sh): lenv → relation term ≝
+| sta_sort: ∀L,k. sta h L (⋆k) (⋆(next h k))
+| sta_ldef: ∀L,K,V,W,U,i. ⇩[0, i] L ≡ K. ⓓV → sta h K V W →
+            ⇧[0, i + 1] W ≡ U → sta h L (#i) U
+| sta_ldec: ∀L,K,W,V,U,i. ⇩[0, i] L ≡ K. ⓛW → sta h K W V →
+            ⇧[0, i + 1] W ≡ U → sta h L (#i) U
+| sta_bind: ∀I,L,V,T,U. sta h (L. ⓑ{I} V) T U →
+            sta h L (ⓑ{I}V.T) (ⓑ{I}V.U)
+| sta_appl: ∀L,V,T,U. sta h L T U →
+            sta h L (ⓐV.T) (ⓐV.U)
+| sta_cast: ∀L,T,U. sta h L T U → sta h L (ⓣU. T) U
+.
+
+interpretation "static type assignment (term)"
+   'StaticType h L T U = (sta h L T U).
+
+(* Basic inversion lemmas ************************************************)
+
+fact sta_inv_sort1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀k0. T = ⋆k0 →
+                        U = ⋆(next h k0).
+#h #L #T #U * -L -T -U
+[ #L #k #k0 #H destruct //
+| #L #K #V #W #U #i #_ #_ #_ #k0 #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #k0 #H destruct
+| #I #L #V #T #U #_ #k0 #H destruct
+| #L #V #T #U #_ #k0 #H destruct
+| #L #T #U #_ #k0 #H destruct
+qed.
+
+(* Basic_1: was: sty0_gen_sort *)
+lemma sta_inv_sort1: ∀h,L,U,k. ⦃h, L⦄ ⊢ ⋆k • U → U = ⋆(next h k).
+/2 width=4/ qed-.
+
+fact sta_inv_lref1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀j. T = #j →
+                        (∃∃K,V,W. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V • W &
+                                  ⇧[0, j + 1] W ≡ U
+                        ) ∨
+                        (∃∃K,W,V. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W • V &
+                                  ⇧[0, j + 1] W ≡ U
+                        ).
+#h #L #T #U * -L -T -U
+[ #L #k #j #H destruct
+| #L #K #V #W #U #i #HLK #HVW #HWU #j #H destruct /3 width=6/
+| #L #K #W #V #U #i #HLK #HWV #HWU #j #H destruct /3 width=6/
+| #I #L #V #T #U #_ #j #H destruct
+| #L #V #T #U #_ #j #H destruct
+| #L #T #U #_ #j #H destruct
+]
+qed.
+
+(* Basic_1: was sty0_gen_lref *)
+lemma sta_inv_lref1: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i • U →
+                     (∃∃K,V,W. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V • W &
+                               ⇧[0, i + 1] W ≡ U
+                     ) ∨
+                     (∃∃K,W,V. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W • V &
+                               ⇧[0, i + 1] W ≡ U
+                     ).
+/2 width=3/ qed-.
+
+fact sta_inv_bind1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀J,X,Y. T = ⓑ{J}Y.X →
+                        ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X • Z & U = ⓑ{J}Y.Z.
+#h #L #T #U * -L -T -U
+[ #L #k #J #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #J #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #J #X #Y #H destruct
+| #I #L #V #T #U #HTU #J #X #Y #H destruct /2 width=3/
+| #L #V #T #U #_ #J #X #Y #H destruct
+| #L #T #U #_ #J #X #Y #H destruct
+]
+qed.
+
+(* Basic_1: was: sty0_gen_bind *)
+lemma sta_inv_bind1: ∀h,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X • U →
+                     ∃∃Z. ⦃h, L.ⓑ{J}Y⦄ ⊢ X • Z & U = ⓑ{J}Y.Z.
+/2 width=3/ qed-.
+
+fact sta_inv_appl1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀X,Y. T = ⓐY.X →
+                        ∃∃Z. ⦃h, L⦄ ⊢ X • Z & U = ⓐY.Z.
+#h #L #T #U * -L -T -U
+[ #L #k #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #X #Y #H destruct
+| #I #L #V #T #U #_ #X #Y #H destruct
+| #L #V #T #U #HTU #X #Y #H destruct /2 width=3/
+| #L #T #U #_ #X #Y #H destruct
+]
+qed.
+
+(* Basic_1: was: sty0_gen_appl *)
+lemma sta_inv_appl1: ∀h,L,Y,X,U. ⦃h, L⦄ ⊢ ⓐY.X • U →
+                     ∃∃Z. ⦃h, L⦄ ⊢ X • Z & U = ⓐY.Z.
+/2 width=3/ qed-.
+
+fact sta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∀X,Y. T = ⓣY.X →
+                     ⦃h, L⦄ ⊢ X • Y ∧ U = Y.
+#h #L #T #U * -L -T -U
+[ #L #k #X #Y #H destruct
+| #L #K #V #W #U #i #_ #_ #_ #X #Y #H destruct
+| #L #K #W #V #U #i #_ #_ #_ #X #Y #H destruct
+| #I #L #V #T #U #_ #X #Y #H destruct
+| #L #V #T #U #_ #X #Y #H destruct
+| #L #T #U #HTU #X #Y #H destruct /2 width=1/
+]
+qed.
+
+(* Basic_1: was: sty0_gen_cast *)
+lemma sta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X • U →  ⦃h, L⦄ ⊢ X • Y ∧ U = Y.
+/2 width=3/ qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sta_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sta_lift.ma
new file mode 100644
index 000000000..1c624e145
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/sta_lift.ma
@@ -0,0 +1,122 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/substitution/ldrop_ldrop.ma".
+include "basic_2/static/sta.ma".
+
+(* STATIC TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Properties on relocation *************************************************)
+
+(* Basic_1: was: sty0_lift *)
+lemma sta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 • U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
+                ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 • U2.
+#h #L1 #T1 #U1 #H elim H -L1 -T1 -U1
+[ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  >(lift_inv_sort1 … H1) -X1
+  >(lift_inv_sort1 … H2) -X2 //
+| #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+  elim (lift_inv_lref1 … H) * #Hid #H destruct
+  [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2
+    elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+    elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
+    /3 width=8/
+  | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+    lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+  ]
+| #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
+  elim (lift_inv_lref1 … H) * #Hid #H destruct
+  [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // <minus_plus #W #HW1 #HWU2
+    elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
+    elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #W2 #HK21 #HW12 #H destruct
+    lapply (lift_mono … HW1 … HW12) -HW1 #H destruct
+    elim (lift_total V1 (d-i-1) e) /3 width=8/
+  | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
+    lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
+  ]
+| #I #L1 #V1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+  elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+  lapply (lift_mono … H1 … HV12) -H1 #H destruct /4 width=5/
+| #L1 #V1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
+  elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
+  elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
+  lapply (lift_mono … H1 … HV12) -H1 #H destruct /4 width=5/
+| #L1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL21 #X #H #U2 #HU12
+  elim (lift_inv_flat1 … H) -H #X2 #T2 #HUX2 #HT12 #H destruct
+  lapply (lift_mono … HUX2 … HU12) -HUX2 #H destruct /3 width=5/
+]
+qed.
+
+(* Note: apparently this was missing in basic_1 *)
+lemma sta_inv_lift: ∀h,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 • U2 → ∀L1,d,e. ⇩[d, e] L2 ≡ L1 →
+                    ∀T1. ⇧[d, e] T1 ≡ T2 →
+                    ∃∃U1. ⦃h, L1⦄ ⊢ T1 • U1 & ⇧[d, e] U1 ≡ U2.
+#h #L2 #T2 #U2 #H elim H -L2 -T2 -U2
+[ #L2 #k #L1 #d #e #_ #X #H
+  >(lift_inv_sort2 … H) -X /2 width=3/
+| #L2 #K2 #V2 #W2 #W #i #HLK2 #HVW2 #HW2 #IHVW2 #L1 #d #e #HL21 #X #H
+  elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HVW2 | -IHVW2 ]
+  [ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // #K1 #V1 #HLK1 #HK21 #HV12
+    elim (IHVW2 … HK21 … HV12) -K2 -V2 #W1 #HVW1 #HW12
+    elim (lift_trans_le … HW12 … HW2 ?) -W2 // >minus_plus <plus_minus_m_m // -Hid /3 width=6/
+  | lapply (ldrop_conf_ge … HL21 … HLK2 ?) -L2 // #HL1K2
+    elim (le_inv_plus_l … Hid) -Hid #Hdie #ei
+    elim (lift_split … HW2 d (i-e+1) ? ? ?) -HW2 // [3: /2 width=1/ ]
+    [ #W0 #HW20 <le_plus_minus_comm // >minus_minus_m_m /2 width=1/ /3 width=6/
+    | <le_plus_minus_comm // /2 width=1/
+    ]
+  ]
+| #L2 #K2 #W2 #V2 #W #i #HLK2 #HWV2 #HW2 #IHWV2 #L1 #d #e #HL21 #X #H
+  elim (lift_inv_lref2 … H) * #Hid #H destruct [ -HWV2 | -IHWV2 ]
+  [ elim (ldrop_conf_lt … HL21 … HLK2 ?) -L2 // #K1 #W1 #HLK1 #HK21 #HW12
+    elim (IHWV2 … HK21 … HW12) -K2 #V1 #HWV1 #_
+    elim (lift_trans_le … HW12 … HW2 ?) -W2 // >minus_plus <plus_minus_m_m // -Hid /3 width=6/
+  | lapply (ldrop_conf_ge … HL21 … HLK2 ?) -L2 // #HL1K2
+    elim (le_inv_plus_l … Hid) -Hid #Hdie #ei
+    elim (lift_split … HW2 d (i-e+1) ? ? ?) -HW2 // [3: /2 width=1/ ]
+    [ #W0 #HW20 <le_plus_minus_comm // >minus_minus_m_m /2 width=1/ /3 width=6/
+    | <le_plus_minus_comm // /2 width=1/
+    ]
+  ]
+| #I #L2 #V2 #T2 #U2 #_ #IHTU2 #L1 #d #e #HL21 #X #H
+  elim (lift_inv_bind2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
+  elim (IHTU2 (L1.ⓑ{I}V1) … HT12) -IHTU2 -HT12 /2 width=1/ -HL21 /3 width=5/
+| #L2 #V2 #T2 #U2 #_ #IHTU2 #L1 #d #e #HL21 #X #H
+  elim (lift_inv_flat2 … H) -H #V1 #T1 #HV12 #HT12 #H destruct
+  elim (IHTU2 … HL21 … HT12) -L2 -HT12 /3 width=5/
+| #L2 #T2 #U2 #_ #IHTU2 #L1 #d #e #HL21 #X #H
+  elim (lift_inv_flat2 … H) -H #U1 #T1 #HU12 #HT12 #H destruct
+  elim (IHTU2 … HL21 … HT12) -L2 -HT12 #U0 #HTU0 #HU02
+  lapply (lift_inj … HU02 … HU12) -HU02 #H destruct /3 width=3/
+]
+qed.  
+
+(* Advanced forvard lemmas **************************************************)
+
+(* Basic_1: was: sty0_correct *)
+lemma sta_fwd_correct: ∀h,L,T,U. ⦃h, L⦄ ⊢ T • U → ∃T0. ⦃h, L⦄ ⊢ U • T0.
+#h #L #T #U #H elim H -L -T -U
+[ /2 width=2/
+| #L #K #V #W #W0 #i #HLK #_ #HW0 * #V0 #HWV0
+  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  elim (lift_total V0 0 (i+1)) /3 width=10/
+| #L #K #W #V #V0 #i #HLK #HWV #HWV0 #_
+  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  elim (lift_total V 0 (i+1)) /3 width=10/
+| #I #L #V #T #U #_ * /3 width=2/
+| #L #V #T #U #_ * #T0 #HUT0 /3 width=2/
+| #L #T #U #_ * /2 width=2/
+]
+qed-.
diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/sta_sta.ma b/matita/matita/contribs/lambda_delta/basic_2/static/sta_sta.ma
new file mode 100644
index 000000000..cee17f8df
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/sta_sta.ma
@@ -0,0 +1,44 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/substitution/ldrop_ldrop.ma".
+include "basic_2/static/sta.ma".
+
+(* STATIC TYPE ASSIGNMENT ON TERMS ******************************************)
+
+(* Main properties **********************************************************)
+
+(* Note: apparently this was missing in basic_1 *)
+theorem sta_mono: ∀h,L,T,U1. ⦃h, L⦄ ⊢ T • U1 →
+                  ∀U2. ⦃h, L⦄ ⊢ T • U2 → U1 = U2.
+#h #L #T #U1 #H elim H -L -T -U1
+[ #L #k #X #H >(sta_inv_sort1 … H) -X //
+| #L #K #V #W #U1 #i #HLK #_ #HWU1 #IHVW #U2 #H
+  elim (sta_inv_lref1 … H) -H * #K0 #V0 #W0 #HLK0 #HVW0 #HW0U2
+  lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct
+  lapply (IHVW … HVW0) -IHVW -HVW0 #H destruct
+  >(lift_mono … HWU1 … HW0U2) -W0 -U1 //
+| #L #K #W #V #U1 #i #HLK #_ #HWU1 #IHWV #U2 #H
+  elim (sta_inv_lref1 … H) -H * #K0 #W0 #V0 #HLK0 #HWV0 #HV0U2
+  lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct
+  lapply (IHWV … HWV0) -IHWV -HWV0 #H destruct
+  >(lift_mono … HWU1 … HV0U2) -W -U1 //
+| #I #L #V #T #U1 #_ #IHTU1 #X #H
+  elim (sta_inv_bind1 … H) -H #U2 #HTU2 #H destruct /3 width=1/
+| #L #V #T #U1 #_ #IHTU1 #X #H
+  elim (sta_inv_appl1 … H) -H #U2 #HTU2 #H destruct /3 width=1/
+| #L #T #U1 #_ #_ #U2 #H
+  elim (sta_inv_cast1 … H) -H //
+]
+qed-.
diff --git a/matita/matita/lib/arithmetics/nat.ma b/matita/matita/lib/arithmetics/nat.ma
index 31d5ced7f..d806697b8 100644
--- a/matita/matita/lib/arithmetics/nat.ma
+++ b/matita/matita/lib/arithmetics/nat.ma
@@ -666,6 +666,9 @@ lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
 #b #c #a #H >(plus_minus_m_m b c) in ⊢ (? ? ?%); //
 qed.
 
+lemma minus_minus_m_m: ∀m,n. n ≤ m → m - (m - n) = n.
+/2 width=1/ qed.
+
 (* Stilll more atomic conclusion ********************************************)
 
 (* le *)
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index b276fe4bb..cbdafb2e0 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