X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fcomputation%2Fcprs_tstc_vector.ma;h=8babd61baf1314bccdfb2b8e6a1849104bbd96d8;hb=08cb57944c0df08611d4f35d286e46c0d13e4813;hp=fd3eb585e2e97d1ae456f82f56aa1dd8654cf174;hpb=9245402674a791dfdb943902f8288d742088c854;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma
index fd3eb585e..8babd61ba 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_tstc_vector.ma
@@ -130,7 +130,7 @@ elim (cprs_inv_appl1 … H) -H *
       @(cprs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) [ /3 width=3/ ] -V1a /3 width=1/
     ]
   ]
-]  
+]
 qed-.
 
 (* Basic_1: was: pr3_iso_appls_cast *)