X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fstatic%2Fssta_ssta.ma;h=a9c027cc68c0f8a5ee50dfa890ea092fc51677c5;hb=9f7f534a11f08bb66815eddf957959eb0eaeb71f;hp=5e699fd557d88c67e92b1678ea5c3ebdaf68e618;hpb=b074ebf6441993694c6e39e4eaeeb58a3186f479;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 5e699fd55..a9c027cc6 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
@@ -36,7 +36,7 @@ theorem ssta_mono: ∀h,g,L,T,U1,l1. ⦃h, L⦄ ⊢ T •[g, l1] U1 →
   lapply (ldrop_mono … HLK0 … HLK) -HLK -HLK0 #H destruct
   lapply (IHWV … HWV0) -IHWV -HWV0 * #H1 #H2 destruct
   >(lift_mono … HWU1 … HV0U2) -W -U1 /2 width=1/
-| #I #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H
+| #a #I #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H
   elim (ssta_inv_bind1 … H) -H #U2 #HTU2 #H destruct
   elim (IHTU1 … HTU2) -T /3 width=1/
 | #L #V #T #U1 #l1 #_ #IHTU1 #X #l2 #H