X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Funfold%2Flstas_alt.ma;h=0ad7b9bbcaf6be208e40e1cbb3b8e62daa69be97;hb=52e675f555f559c047d5449db7fc89a51b977d35;hp=17e048a631cfa06819f537d342146eb474db7a76;hpb=75fac6d60f67a4dfa38ea6c2cc45a18eda5d8996;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_alt.ma
index 17e048a63..0ad7b9bbc 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lstas_alt.ma
@@ -47,10 +47,10 @@ lemma lstasa_step_dx: ∀h,G,L,T1,T,l. ⦃G, L⦄ ⊢ T1 ••*[h, l] T →
 [ /2 width=1 by sta_lstasa/
 | #G #L #l #k #X #H >(sta_inv_sort1 … H) -X >commutative_plus //
 | #G #L #K #V #W #U #i #l #HLK #_ #HWU #IHVW #U2 #HU2
-  lapply (ldrop_fwd_drop2 … HLK) #H
+  lapply (drop_fwd_drop2 … HLK) #H
   elim (sta_inv_lift1 … HU2 … H … HWU) -H -U /3 width=6 by lstasa_ldef/
 | #G #L #K #W #V #V0 #U #i #l #HLK #HWl0 #_ #HVU #IHWV #U2 #HU2
-  lapply (ldrop_fwd_drop2 … HLK) #H
+  lapply (drop_fwd_drop2 … HLK) #H
   elim (sta_inv_lift1 … HU2 … H … HVU) -H -U /3 width=8 by lstasa_ldec/
 | #a #I #G #L #V #T1 #U1 #l #_ #IHTU1 #X #H
   elim (sta_inv_bind1 … H) -H #U #HU1 #H destruct /3 width=1 by lstasa_bind/