- we introduced the pointer_step rc in the perspective of proving

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / substitution / ldrop_append.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_append.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_append.ma
index 3f6b2c53816ea3ed1a0b636b9eb2ae70a9e1196d..359d39c80c4ea0a59c82a9809a79504730cb1a29 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_append.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop_append.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/grammar/lenv_append.ma".
 include "basic_2/substitution/ldrop.ma".
 
 (* DROPPING *****************************************************************)
@@ -31,6 +30,8 @@ lemma ldrop_O1_append_sn_le: ∀L1,L2,e. ⇩[0, e] L1 ≡ L2 → e ≤ |L1| →
                              ∀L. ⇩[0, e] L @@ L1 ≡ L @@ L2.
 /2 width=3 by ldrop_O1_append_sn_le_aux/ qed.
 
+(* Inversion lemmas on append for local environments ************************)
+
 lemma ldrop_O1_inv_append1_ge: ∀K,L1,L2,e. ⇩[0, e] L1 @@ L2 ≡ K →
                                |L2| ≤ e → ⇩[0, e - |L2|] L1 ≡ K.
 #K #L1 #L2 elim L2 -L2 normalize //