- we introduced the pointer_step rc in the perspective of proving

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / static / ssta_ssta.ma

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 5e699fd557d88c67e92b1678ea5c3ebdaf68e618..b20e4366a631a19f554390189cfeb94bc14f61a9 100644 (file)
--- 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,15 +36,14 @@ 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
   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-.