- lib: some additions

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / computation / csn_tstc_vector.ma

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma
index 3aa7170f50da7ca220c06e2c529fa290cf4636b6..e1a64150599580ba687f254c81f3e33ce4ebe60c 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_tstc_vector.ma
@@ -81,7 +81,7 @@ lapply (csn_appl_theta … HW12 … H) -H -HW12 #H
 lapply (csn_fwd_pair_sn … H) #HW1
 lapply (csn_fwd_flat_dx … H) #H1
 @csn_appl_simple_tstc // -HW1 /2 width=3/ -IHV12s -HV -H1 #X #H1 #H2
-elim (cprs_fwd_theta_vector … (V2::V2s) … H1) -H1 /2 width=1/ -HV12s -HV12
+elim (cprs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1/ -HV12s -HV12
 [ -H #H elim (H2 ?) -H2 //
 | -H2 #H1 @(csn_cprs_trans … H) -H /2 width=1/
 ]