X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Fterm_vector.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fsyntax%2Fterm_vector.ma;h=8be2b3ae723acfe3513b8133e0f6d75bdd65ede9;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=82581af61bc71ed7e62272a456625c4dd9f39196;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/term_vector.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/term_vector.ma
index 82581af61..8be2b3ae7 100644
--- a/matita/matita/contribs/lambdadelta/static_2/syntax/term_vector.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/syntax/term_vector.ma
@@ -37,6 +37,6 @@ lemma applv_cons: ∀V,Vs,T. ⒶV⨮Vs.T = ⓐV.ⒶVs.T.
 
 (* Properties with simple terms *********************************************)
 
-lemma applv_simple: ∀T,Vs. 𝐒❪T❫ → 𝐒❪ⒶVs.T❫.
+lemma applv_simple: ∀T,Vs. 𝐒❨T❩ → 𝐒❨ⒶVs.T❩.
 #T * //
 qed.