X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fstatic%2Fssta_ssta.ma;h=b20e4366a631a19f554390189cfeb94bc14f61a9;hb=6c86c70b005e3f3efd375868b27f3cff84febfad;hp=a9c027cc68c0f8a5ee50dfa890ea092fc51677c5;hpb=a2144f09d1bd7022c1f2dfd4909a1fb9772c8d56;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ssta.ma b/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ssta.ma
index a9c027cc6..b20e4366a 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ssta.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/static/ssta_ssta.ma
@@ -42,9 +42,8 @@ theorem ssta_mono: ∀h,g,L,T,U1,l1. ⦃h, L⦄ ⊢ T •[g, l1] U1 →
 | #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H
   elim (ssta_inv_appl1 … H) -H #U2 #HTU2 #H destruct
   elim (IHTU1 … HTU2) -T /3 width=1/
-| #L #V #W1 #T #U1 #l1 #_ #_ #IHVW1 #IHTU1 #U2 #l2 #H
-  elim (ssta_inv_cast1 … H) -H #W2 #T2 #HVW2 #HTU2 #H destruct
-  elim (IHVW1 … HVW2) -V
+| #L #W1 #T #U1 #l1 #_ #IHTU1 #U2 #l2 #H
+  lapply (ssta_inv_cast1 … H) -H #HTU2
   elim (IHTU1 … HTU2) -T /2 width=1/
 ]
 qed-.