X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Falpha_1%2Fsyntax%2Fterm_append.ma;h=63ddda16f9622d4fb2c390000dfb1de20bdfed51;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hp=4ea795a68d65fca1402cf8148e96abffa6eec155;hpb=09b4420070d6a71990e16211e499b51dbb0742cb;p=helm.git

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 4ea795a68..63ddda16f 100644
--- 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)" 'Append T U = (tappend T U).
+interpretation "append (term)" 'plus T U = (tappend T U).