X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Flleq.ma;h=72a5346ce6d588fccec627621b86788ce16fb0af;hb=d95bd78c09617ad212fa9e96837a15fc907dcfca;hp=6bce82987cb7ba527555881b4ed35fb2b2ef09ab;hpb=e2527c6784c2593ca67af35fafaf0b3725d80a60;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
index 6bce82987..72a5346ce 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
@@ -66,7 +66,7 @@ lemma lleq_be: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 → ∀T,d,e. ⇧[d, e] T ≡ U 
                d ≤ dt → dt ≤ d + e → L1 ⋕[U, d] L2.
 #L1 #L2 #U #dt * #HL12 #IH #T #d #e #HTU #Hddt #Hdtde @conj // -HL12
 #U0 elim (IH U0) -IH #H12 #H21 @conj
-#HU0 elim (cpys_up … HU0 … HTU) // -HU0 /4 width=5 by cpys_weak/
+#HU0 elim (cpys_fwd_up … HU0 … HTU) // -HU0 /4 width=5 by cpys_weak/
 qed-.
 
 lemma lsuby_lleq_trans: ∀L2,L,T,d. L2 ⋕[T, d] L →