first main property of drop closed

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

diff --git a/matita/matita/lib/lambda-delta/substitution/drop_defs.ma b/matita/matita/lib/lambda-delta/substitution/drop_defs.ma
index 0644efdbeea77ebfaceed993c1ce8458be24f788..79af8f90da46c25c42e4d9c2f4ba3f0a757f3bea 100644 (file)
--- a/matita/matita/lib/lambda-delta/substitution/drop_defs.ma
+++ b/matita/matita/lib/lambda-delta/substitution/drop_defs.ma
@@ -26,14 +26,27 @@ interpretation "dropping" 'RLift L2 d e L1 = (drop L1 d e L2).
 
 (* the basic inversion lemmas ***********************************************)
 
+lemma drop_inv_drop1_aux: ∀d,e,L2,L1. ↑[d, e] L2 ≡ L1 → 0 < e → d = 0 →
+                          ∀K,I,V. L1 = K. 𝕓{I} V → ↑[d, e - 1] L2 ≡ K.
+#d #e #L2 #L1 #H elim H -H d e L2 L1
+[ #L #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V #e #HL12 #_ #_ #_ #K #J #W #H destruct -L1 I V //
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #_ #_ #H elim (plus_S_eq_O_false … H)
+]
+qed.
+
+lemma drop_inv_drop1: ∀e,L2,K,I,V. ↑[0, e] L2 ≡ K. 𝕓{I} V → 0 < e →
+                                   ↑[0, e - 1] L2 ≡ K.
+/2 width=5/ qed.
+
 lemma drop_inv_skip2_aux: ∀d,e,L1,L2. ↑[d, e] L2 ≡ L1 → 0 < d →
                           ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
                           ∃∃K1,V1. ↑[d - 1, e] K2 ≡ K1 &
                                    ↑[d - 1, e] V2 ≡ V1 & 
                                    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/
 ]