update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / alpha_1 / syntax / term_append.ma

diff --git a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma b/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma
index a2db5fedd6cf1b23104a5fb0d0237dcc66c9df53..63ddda16f9622d4fb2c390000dfb1de20bdfed51 100644 (file)
--- a/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma
+++ b/matita/matita/contribs/lambdadelta/alpha_1/syntax/term_append.ma
@@ -18,8 +18,8 @@ include "alpha_1/syntax/term.ma".
 
 let rec tappend T U on T ≝ match T with
 [ TAtom       ⇒ U
-| TUnit I T   ⇒ ①{I}.(tappend T U)
-| TPair I V T ⇒ ②{I}V.(tappend T U)
+| TUnit I T   ⇒ ①[I].(tappend T U)
+| TPair I V T ⇒ ②[I]V.(tappend T U)
 ].
 
 interpretation "append (term)" 'plus T U = (tappend T U).