X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Fcpys.ma;h=7da756f978ea3f7827363cc7bc865e2b8d08dfc7;hb=658c000ee2ea2da04cf29efc0acdaf16364fbf5e;hp=2ca575e2af32758a09fee8a4db30877422fa321b;hpb=1994fe8e6355243652770f53a02db5fdf26915f0;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma
index 2ca575e2a..7da756f97 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/cpys.ma
@@ -159,8 +159,8 @@ lemma cpys_inv_refl_O2: ∀G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 ▶*[l, 0] T2 → T1 =
 #T #T2 #_ #HT2 #IHT1 <(cpy_inv_refl_O2 … HT2) -HT2 //
 qed-.
 
-lemma cpys_inv_lift1_eq: ∀G,L,U1,U2. ∀l,m:nat.
-                         ⦃G, L⦄ ⊢ U1 ▶*[l, m] U2 → ∀T1. ⬆[l, m] T1 ≡ U1 → U1 = U2.
+lemma cpys_inv_lift1_eq: ∀G,L,U1,U2,l,m.
+                         ⦃G, L⦄ ⊢ U1 ▶*[l, yinj m] U2 → ∀T1. ⬆[l, m] T1 ≡ U1 → U1 = U2.
 #G #L #U1 #U2 #l #m #H #T1 #HTU1 @(cpys_ind … H) -U2
 /2 width=7 by cpy_inv_lift1_eq/
 qed-.