X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fsnv_lstas.ma;h=de2cf0d7a0a0381d933c73a8dcd26f8a0cfb1fdb;hb=52e675f555f559c047d5449db7fc89a51b977d35;hp=53641051d18f0d76da872a422a0baabd4f26e041;hpb=75fac6d60f67a4dfa38ea6c2cc45a18eda5d8996;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma
index 53641051d..de2cf0d7a 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lstas.ma
@@ -32,12 +32,12 @@ fact snv_lstas_aux: ∀h,g,G0,L0,T0.
   [ lapply (lstas_inv_O … H2) -H2 #H destruct // ]
   elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #HLK0 #HX0
   elim (da_inv_lref … Hl1) -Hl1 * #K1 [ #V1 | #W1 #l ] #HLK1 [ #Hl1 | #Hl #H ]
-  lapply (ldrop_mono … HLK0 … HLK1) -HLK0 #H0 destruct
+  lapply (drop_mono … HLK0 … HLK1) -HLK0 #H0 destruct
   elim (lstas_inv_lref1 … H2) -H2 * #K0 #Y0 #X0 [2,4: #Y1 ] #HLK0 [1,2: #HY01 ] #HYX0 #HX0
-  lapply (ldrop_mono … HLK0 … HLK1) -HLK0 #H destruct
+  lapply (drop_mono … HLK0 … HLK1) -HLK0 #H destruct
   [ lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21 ]
   lapply (fqup_lref … G1 … HLK1) #H
-  lapply (ldrop_fwd_drop2 … HLK1) -HLK1 /4 width=8 by fqup_fpbg, snv_lift/
+  lapply (drop_fwd_drop2 … HLK1) -HLK1 /4 width=8 by fqup_fpbg, snv_lift/
 | #p #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1
   elim (snv_inv_gref … H1)
 | #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2