X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fcomputation%2Fcsn_vector.ma;h=7c26ef429234e39edae390971089dda75455a69c;hb=f7386d0b74f935f07ede4be46d0489a233d68b85;hp=a8663d8ba7138e98830de9c1048d0ef95229c4bd;hpb=7cf0b6c720e4d7fa05dd25ec0ad0478c0802ba67;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma
index a8663d8ba..7c26ef429 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_vector.ma
@@ -26,5 +26,5 @@ interpretation
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬇* T :: Ts → L ⊢ ⬇* T ∧ L ⊢ ⬇* Ts.
+lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬊* T @ Ts → L ⊢ ⬊* T ∧ L ⊢ ⬊* Ts.
 normalize // qed-.