- 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 66852c667b6f4fcd0e76cc26387070320b41b420..a1e538ae09e342b3fa184c6411fa11c04407b485 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma
@@ -41,7 +41,7 @@ lemma lsuby_cpy_trans: ∀G,d,e. lsub_trans … (cpy d e G) (lsuby d e).
 #G #d #e #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 -d -e
 [ //
 | #I #G #L1 #K1 #V #W #i #d #e #Hdi #Hide #HLK1 #HVW #L2 #HL12
-  elim (lsuby_fwd_ldrop2_be … HL12 … HLK1) -HL12 -HLK1 /2 width=5 by cpy_subst/
+  elim (lsuby_ldrop_trans_be … HL12 … HLK1) -HL12 -HLK1 /2 width=5 by cpy_subst/
 | /4 width=1 by lsuby_succ, cpy_bind/
 | /3 width=1 by cpy_flat/
 ]