X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2A%2Fsubstitution%2Flift_lift.ma;h=3a3871d2039eb57f09784b139b769dc25709ec16;hb=2f6f2b7c01d47d23f61dd48d767bcb37aecdcfea;hp=bbc747aa7af6308d904f5fca908197f54f5fa08e;hpb=d2545ffd201b1aa49887313791386add78fa8603;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2A/substitution/lift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2A/substitution/lift_lift.ma
index bbc747aa7..3a3871d20 100644
--- a/matita/matita/contribs/lambdadelta/basic_2A/substitution/lift_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2A/substitution/lift_lift.ma
@@ -18,7 +18,6 @@ include "basic_2A/substitution/lift.ma".
 
 (* Main properties ***********************************************************)
 
-(* Basic_1: was: lift_inj *)
 theorem lift_inj: ∀l,m,T1,U. ⬆[l,m] T1 ≡ U → ∀T2. ⬆[l,m] T2 ≡ U → T1 = T2.
 #l #m #T1 #U #H elim H -l -m -T1 -U
 [ #k #l #m #X #HX
@@ -36,7 +35,6 @@ theorem lift_inj: ∀l,m,T1,U. ⬆[l,m] T1 ≡ U → ∀T2. ⬆[l,m] T2 ≡ U 
 ]
 qed-.
 
-(* Basic_1: was: lift_gen_lift *)
 theorem lift_div_le: ∀l1,m1,T1,T. ⬆[l1, m1] T1 ≡ T →
                      ∀l2,m2,T2. ⬆[l2 + m1, m2] T2 ≡ T →
                      l1 ≤ l2 →
@@ -69,7 +67,6 @@ theorem lift_div_le: ∀l1,m1,T1,T. ⬆[l1, m1] T1 ≡ T →
 ]
 qed.
 
-(* Note: apparently this was missing in basic_1 *)
 theorem lift_div_be: ∀l1,m1,T1,T. ⬆[l1, m1] T1 ≡ T →
                      ∀m,m2,T2. ⬆[l1 + m, m2] T2 ≡ T →
                      m ≤ m1 → m1 ≤ m + m2 →
@@ -116,7 +113,6 @@ theorem lift_mono: ∀l,m,T,U1. ⬆[l,m] T ≡ U1 → ∀U2. ⬆[l,m] T ≡ U2 
 ]
 qed-.
 
-(* Basic_1: was: lift_free (left to right) *)
 theorem lift_trans_be: ∀l1,m1,T1,T. ⬆[l1, m1] T1 ≡ T →
                        ∀l2,m2,T2. ⬆[l2, m2] T ≡ T2 →
                        l1 ≤ l2 → l2 ≤ l1 + m1 → ⬆[l1, m1 + m2] T1 ≡ T2.
@@ -136,7 +132,7 @@ theorem lift_trans_be: ∀l1,m1,T1,T. ⬆[l1, m1] T1 ≡ T →
 | #a #I #V1 #V2 #T1 #T2 #l1 #m1 #_ #_ #IHV12 #IHT12 #l2 #m2 #X #HX #Hl12 #Hl21
   elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct 
   lapply (IHV12 … HV20 ? ?) // -IHV12 -HV20 #HV10
-  lapply (IHT12 … HT20 ? ?) /2 width=1 by lift_bind, le_S_S/ (**) (* full auto a bit slow *)
+  lapply (IHT12 … HT20 ? ?) /2 width=1 by lift_bind, monotonic_le_plus_l, le_S_S/ (* full auto a bit slow *)
 | #I #V1 #V2 #T1 #T2 #l1 #m1 #_ #_ #IHV12 #IHT12 #l2 #m2 #X #HX #Hl12 #Hl21
   elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct
   lapply (IHV12 … HV20 ? ?) // -IHV12 -HV20 #HV10
@@ -144,7 +140,6 @@ theorem lift_trans_be: ∀l1,m1,T1,T. ⬆[l1, m1] T1 ≡ T →
 ]
 qed.
 
-(* Basic_1: was: lift_d (right to left) *)
 theorem lift_trans_le: ∀l1,m1,T1,T. ⬆[l1, m1] T1 ≡ T →
                        ∀l2,m2,T2. ⬆[l2, m2] T ≡ T2 → l2 ≤ l1 →
                        ∃∃T0. ⬆[l2, m2] T1 ≡ T0 & ⬆[l1 + m2, m1] T0 ≡ T2.
@@ -171,7 +166,6 @@ theorem lift_trans_le: ∀l1,m1,T1,T. ⬆[l1, m1] T1 ≡ T →
 ]
 qed.
 
-(* Basic_1: was: lift_d (left to right) *)
 theorem lift_trans_ge: ∀l1,m1,T1,T. ⬆[l1, m1] T1 ≡ T →
                        ∀l2,m2,T2. ⬆[l2, m2] T ≡ T2 → l1 + m1 ≤ l2 →
                        ∃∃T0. ⬆[l2 - m1, m2] T1 ≡ T0 & ⬆[l1, m1] T0 ≡ T2.
@@ -190,7 +184,7 @@ theorem lift_trans_ge: ∀l1,m1,T1,T. ⬆[l1, m1] T1 ≡ T →
 | #a #I #V1 #V2 #T1 #T2 #l1 #m1 #_ #_ #IHV12 #IHT12 #l2 #m2 #X #HX #Hlml
   elim (lift_inv_bind1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct
   elim (IHV12 … HV20) -IHV12 -HV20 //
-  elim (IHT12 … HT20) -IHT12 -HT20 /2 width=1 by le_S_S/ #T
+  elim (IHT12 … HT20) -IHT12 -HT20 [2: <assoc_plus1 /2 width=1 by le_S_S/ ]
   <plus_minus /3 width=5 by lift_bind, le_plus_to_minus_r, le_plus_b, ex2_intro/
 | #I #V1 #V2 #T1 #T2 #l1 #m1 #_ #_ #IHV12 #IHT12 #l2 #m2 #X #HX #Hlml
   elim (lift_inv_flat1 … HX) -HX #V0 #T0 #HV20 #HT20 #HX destruct