- slicing relation for the global environment defined (gdrop)

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / substitution / lift.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma
index f58c1906e449b098da320dad10d28ec99bef31e6..fa1dfae280dec03d5f8fc66d5a6c43e3d88af8b6 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/lift.ma
@@ -164,7 +164,8 @@ lemma lift_inv_lref2: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i →
 lemma lift_inv_lref2_lt: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → i < d → T1 = #i.
 #d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * //
 #Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi -Hid #Hdd
-elim (plus_lt_false … Hdd)
+elim (lt_inv_plus_l … Hdd) -Hdd #Hdd
+elim (lt_refl_false … Hdd)
 qed-.
 
 (* Basic_1: was: lift_gen_lref_false *)
@@ -180,7 +181,8 @@ qed-.
 lemma lift_inv_lref2_ge: ∀d,e,T1,i. ↑[d,e] T1 ≡ #i → d + e ≤ i → T1 = #(i - e).
 #d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * //
 #Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi -Hid #Hdd
-elim (plus_lt_false … Hdd)
+elim (lt_inv_plus_l … Hdd) -Hdd #Hdd
+elim (lt_refl_false … Hdd)
 qed-.
 
 fact lift_inv_gref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀p. T2 = §p → T1 = §p.
@@ -303,8 +305,8 @@ lemma lift_split: ∀d1,e2,T1,T2. ↑[d1, e2] T1 ≡ T2 →
 | #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_
   lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 /4 width=3/
 | #i #d1 #e2 #Hid1 #d2 #e1 #_ #Hd21 #He12
-  lapply (transitive_le …(i+e1) Hd21 ?) /2 width=1/ -Hd21 #Hd21
-  <(arith_d1 i e2 e1) // /3 width=3/
+  lapply (transitive_le … (i+e1) Hd21 ?) /2 width=1/ -Hd21 #Hd21
+  >(plus_minus_m_m e2 e1 ?) // /3 width=3/
 | /3 width=3/
 | #I #V1 #V2 #T1 #T2 #d1 #e2 #_ #_ #IHV #IHT #d2 #e1 #Hd12 #Hd21 #He12
   elim (IHV … Hd12 Hd21 He12) -IHV #V0 #HV0a #HV0b