more lemmas and some generated logical constants for them

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

diff --git a/matita/matita/lib/lambda-delta/substitution/thin_defs.ma b/matita/matita/lib/lambda-delta/substitution/thin_defs.ma
index 1e78476038e5bde644605047bcf0ab8ff9730643..c8ef449251ec032e8dc96824c7c9f14e5ea35ccb 100644 (file)
--- a/matita/matita/lib/lambda-delta/substitution/thin_defs.ma
+++ b/matita/matita/lib/lambda-delta/substitution/thin_defs.ma
@@ -31,8 +31,8 @@ lemma thin_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d →
                                    K1 ⊢ ↓[d - 1, e] V1 ≡ V2 & 
                                    L1 = K1. 𝕓{I} V1.
 #d #e #L1 #L2 #H elim H -H d e L1 L2
-[ #L #H elim (lt_false … H)
-| #L1 #L2 #I #V #e #_ #_ #H elim (lt_false … H)
+[ #L #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V #e #_ #_ #H elim (lt_refl_false … H)
 | #L1 #X #Y #V1 #Z #d #e #HL12 #HV12 #_ #_ #I #L2 #V2 #H destruct -X Y Z;
   /2 width=5/
 ]