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

diff --git a/matita/matita/lib/lambda-delta/substitution/thin_defs.ma b/matita/matita/lib/lambda-delta/substitution/thin_defs.ma
index 1e7847603..c8ef44925 100644
--- 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/
 ]