X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Fcpts_aaa.ma;h=fb99d63286c236b07c26c1757297612bc7afa14c;hp=a881796a56814842ab9b6f3182efb16ae3d25d5a;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hpb=3b7b8afcb429a60d716d5226a5b6ab0d003228b1

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 a881796a5..fb99d6328 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,24 +20,24 @@ 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
   cases I -I
   [ elim (IH n) -IH #V2 #HV12
-    elim (lifts_total V2 (𝐔❴1❵)) #T2 #HVT2
+    elim (lifts_total V2 (𝐔❨1❩)) #T2 #HVT2
     /3 width=4 by cpts_delta, ex_intro/
   | cases n -n
     [ /2 width=2 by ex_intro/
     | #n elim (IH n) -IH #V2 #HV12
-      elim (lifts_total V2 (𝐔❴1❵)) #T2 #HVT2
+      elim (lifts_total V2 (𝐔❨1❩)) #T2 #HVT2
       /3 width=4 by cpts_ell, ex_intro/
     ]
   ]
 | #I #G #K #A #i #_ #IH #n -A
   elim (IH n) -IH #T #HT
-  elim (lifts_total T (𝐔❴1❵)) #U #HTU
+  elim (lifts_total T (𝐔❨1❩)) #U #HTU
   /3 width=4 by cpts_lref, ex_intro/
 | #p #G #L #V1 #T1 #B #A #_ #_ #IHV #IHT #n -B -A
   elim (IHV 0) -IHV #V2 #HV12