X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcsx_vector.ma;h=5d0552b9522b35d4e143e69d20c294488b002735;hp=6fdda2bbfb0ba80334d3f068698209206b1509b4;hb=a77d0bd6a04e94f765d329d47b37d9e04d349b14;hpb=b598b37379baabef24ae511596be7f740cbb0c2e

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma
index 6fdda2bbf..5d0552b95 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma
@@ -26,7 +26,7 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma csxv_inv_cons: ∀h,o,G,L,T,Ts. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T@Ts⦄ →
+lemma csxv_inv_cons: ∀h,o,G,L,T,Ts. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⨮Ts⦄ →
                      ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ ∧ ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃Ts⦄.
 normalize // qed-.