X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsyntax%2Fterm_vector.ma;h=cbb43ebb21767703a581738458093ec29ffbd3fe;hp=1de2ef35215de1f2092f185704d8555c8961dc8a;hb=a77d0bd6a04e94f765d329d47b37d9e04d349b14;hpb=b598b37379baabef24ae511596be7f740cbb0c2e diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/term_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/term_vector.ma index 1de2ef352..cbb43ebb2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/term_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/term_vector.ma @@ -32,7 +32,7 @@ interpretation "application to vector (term)" lemma applv_nil: ∀T. Ⓐ◊.T = T. // qed. -lemma applv_cons: ∀V,Vs,T. ⒶV@Vs.T = ⓐV.ⒶVs.T. +lemma applv_cons: ∀V,Vs,T. ⒶV⨮Vs.T = ⓐV.ⒶVs.T. // qed. (* Properties with simple terms *********************************************)