more lemmas and some generated logical constants for them

[helm.git] / matita / matita / lib / lambda-delta / substitution / lift_defs.ma

diff --git a/matita/matita/lib/lambda-delta/substitution/lift_defs.ma b/matita/matita/lib/lambda-delta/substitution/lift_defs.ma
index 1f9be7fe2f4aeafb984152b6cfe641e38b7cad4b..472aef80969853afe20f07a93ee6565a702082b1 100644 (file)
--- 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 →