- advances on hereditarily free variables: now "frees" is primitive

[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 cf29f1cc2ba48a5501fd2962faaf89ff07544fa0..a1e538ae09e342b3fa184c6411fa11c04407b485 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
@@ -83,7 +83,6 @@ 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 //