- more properties on strongly normalizing terms

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / grammar / term_vector.ma

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma
index 01dec21029029b8422487c81fddbf73d92fd0f9d..2b3f8880ee2a7152cddbb807a080bc06469dd186 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/grammar/term_vector.ma
@@ -20,7 +20,8 @@ include "Basic_2/grammar/term.ma".
 let rec applv Vs T on Vs ≝
   match Vs with
   [ nil        ⇒ T
-  | cons hd tl ⇒  𝕔{Appl} hd. (applv tl T)
+  | cons hd tl ⇒  ⓐhd. (applv tl T)
   ].
 
-interpretation "application construction (vector)" 'ApplV Vs T = (applv Vs T).
+interpretation "application o vevtor (term)"
+   'SnApplV Vs T = (applv Vs T).