- revision of ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / substitution / cpy_cpy.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_cpy.ma
index ef48b05afeb068fef8ce035b6bbd80808f7b9b35..7a65a2db508121d5693043ecb5e866fa3d790fad 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_cpy.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpy_cpy.ma
@@ -85,7 +85,8 @@ theorem cpy_trans_ge: ∀G,L,T1,T0,l,m. ⦃G, L⦄ ⊢ T1 ▶[l, m] T0 →
   elim (cpy_inv_atom1 … H) -H
   [ #H destruct //
   | * #J #K #V #i #Hl2i #Hilm2 #HLK #HVT2 #H destruct
-    lapply (ylt_yle_trans … (l+m) … Hilm2) /2 width=5 by cpy_subst, monotonic_yle_plus_dx/
+    lapply (ylt_yle_trans … (l+m) … Hilm2)
+    /2 width=5 by cpy_subst, monotonic_yle_plus_sn/
   ]
 | #I #G #L #K #V #V2 #i #l #m #Hli #Hilm #HLK #HVW #T2 #HVT2 #Hm
   lapply (cpy_weak … HVT2 0 (i+1) ? ?) -HVT2 /3 width=1 by yle_plus_dx2_trans, yle_succ/