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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma
index faad2323a..5442d8435 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_vector.ma
@@ -27,15 +27,15 @@ interpretation
 (* Basic inversion lemmas ***************************************************)
 
 lemma csxv_inv_cons (G) (L):
-      ∀T,Ts. ❪G,L❫ ⊢ ⬈*𝐒 T⨮Ts →
-      ∧∧ ❪G,L❫ ⊢ ⬈*𝐒 T & ❪G,L❫ ⊢ ⬈*𝐒 Ts.
+      ∀T,Ts. ❨G,L❩ ⊢ ⬈*𝐒 T⨮Ts →
+      ∧∧ ❨G,L❩ ⊢ ⬈*𝐒 T & ❨G,L❩ ⊢ ⬈*𝐒 Ts.
 normalize // qed-.
 
 (* Basic forward lemmas *****************************************************)
 
 lemma csx_fwd_applv (G) (L):
-      ∀T,Vs. ❪G,L❫ ⊢ ⬈*𝐒 ⒶVs.T →
-      ∧∧ ❪G,L❫ ⊢ ⬈*𝐒 Vs & ❪G,L❫ ⊢ ⬈*𝐒 T.
+      ∀T,Vs. ❨G,L❩ ⊢ ⬈*𝐒 ⒶVs.T →
+      ∧∧ ❨G,L❩ ⊢ ⬈*𝐒 Vs & ❨G,L❩ ⊢ ⬈*𝐒 T.
 #G #L #T #Vs elim Vs -Vs /2 width=1 by conj/
 #V #Vs #IHVs #HVs
 lapply (csx_fwd_pair_sn … HVs) #HV