update in ground_2 and basic_2 ...

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / cpy.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
index 3709db1d7edb93bbf8269b0411e5a90c4d8425f6..cf29f1cc2ba48a5501fd2962faaf89ff07544fa0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
@@ -15,7 +15,7 @@
 include "ground_2/ynat/ynat_max.ma".
 include "basic_2/notation/relations/psubst_6.ma".
 include "basic_2/grammar/genv.ma".
-include "basic_2/relocation/ldrop.ma".
+include "basic_2/relocation/lsuby.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED ORDINARY SUBSTITUTION FOR TERMS ***************)
 
@@ -83,6 +83,7 @@ lemma cpy_weak: ∀G,L,T1,T2,d1,e1. ⦃G, L⦄ ⊢ T1 ▶[d1, e1] T2 →
 ]
 qed-.
 
+(* Note: lemma 1250 *)
 lemma cpy_weak_top: ∀G,L,T1,T2,d,e.
                     ⦃G, L⦄ ⊢ T1 ▶[d, e] T2 → ⦃G, L⦄ ⊢ T1 ▶[d, |L| - d] T2.
 #G #L #T1 #T2 #d #e #H elim H -G -L -T1 -T2 -d -e //