X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpts_aaa.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpts_aaa.ma;h=864c4849527151110673a363b288bbc6b5a5d140;hb=8ec019202bff90959cf1a7158b309e7f83fa222e;hp=fb99d63286c236b07c26c1757297612bc7afa14c;hpb=33d0a7a9029859be79b25b5a495e0f30dab11f37;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_aaa.ma
index fb99d6328..864c48495 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpts_aaa.ma
@@ -20,7 +20,7 @@ include "basic_2/rt_computation/cpts_drops.ma".
 (* Properties with atomic arity assignment for terms ************************)
 
 lemma cpts_total_aaa (h) (G) (L) (T1):
-      ∀A. ❪G,L❫ ⊢ T1 ⁝ A → ∀n. ∃T2. ❪G,L❫ ⊢ T1 ⬆*[h,n] T2.
+      ∀A. ❨G,L❩ ⊢ T1 ⁝ A → ∀n. ∃T2. ❨G,L❩ ⊢ T1 ⬆*[h,n] T2.
 #h #G #L #T1 #A #H elim H -G -L -T1 -A
 [ #G #L #s #n /3 width=2 by ex_intro/
 | #I #G #K #V1 #B #_ #IH #n -B