X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Flambda-delta%2Fsubstitution%2Flift_defs.ma;fp=matita%2Fmatita%2Flib%2Flambda-delta%2Fsubstitution%2Flift_defs.ma;h=472aef80969853afe20f07a93ee6565a702082b1;hb=b4d7d16ff7635d9430e92ba86eaf513a9ad9ff8e;hp=1f9be7fe2f4aeafb984152b6cfe641e38b7cad4b;hpb=1e6b9fe97056bdffc515e1951de67d85d40e964c;p=helm.git

diff --git a/matita/matita/lib/lambda-delta/substitution/lift_defs.ma b/matita/matita/lib/lambda-delta/substitution/lift_defs.ma
index 1f9be7fe2..472aef809 100644
--- a/matita/matita/lib/lambda-delta/substitution/lift_defs.ma
+++ b/matita/matita/lib/lambda-delta/substitution/lift_defs.ma
@@ -79,13 +79,13 @@ lemma lift_inv_lref1: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 →
 lemma lift_inv_lref1_lt: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → i < d → T2 = #i.
 #d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * //
 #Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd
-elim (lt_false … Hdd)
+elim (lt_refl_false … Hdd)
 qed.
 
 lemma lift_inv_lref1_ge: ∀d,e,T2,i. ↑[d,e] #i ≡ T2 → d ≤ i → T2 = #(i + e).
 #d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * //
 #Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi Hid #Hdd
-elim (lt_false … Hdd)
+elim (lt_refl_false … Hdd)
 qed.
 
 lemma lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →