X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fnta_drops.ma;h=86ad0e1e5fdb6b18b3f23800355ffef4cc35c30b;hb=cfd201c62dd9b854bfb4ada648d3e556b29fac3a;hp=5aea37112458352ffde4bf012316034e6c276b76;hpb=bd53c4e895203eb049e75434f638f26b5a161a2b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma
index 5aea37112..86ad0e1e5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.ma
@@ -20,8 +20,8 @@ include "basic_2/dynamic/nta.ma".
 (* Advanced properties ******************************************************)
 
 lemma nta_ldef (h) (a) (G) (K):
-      ∀V,W. ❪G,K❫ ⊢ V :[h,a] W →
-      ∀U. ⇧*[1] W ≘ U → ❪G,K.ⓓV❫ ⊢ #0 :[h,a] U.
+      ∀V,W. ❨G,K❩ ⊢ V :[h,a] W →
+      ∀U. ⇧[1] W ≘ U → ❨G,K.ⓓV❩ ⊢ #0 :[h,a] U.
 #h #a #G #K #V #W #H #U #HWU
 elim (cnv_inv_cast … H) -H #X #HW #HV #HWX #HVX
 lapply (cnv_lifts … HW (Ⓣ) … (K.ⓓV) … HWU) -HW
@@ -32,16 +32,16 @@ elim (cpms_lifts_sn … HWX … (Ⓣ) … (K.ⓓV) … HWU) -W
 qed.
 
 lemma nta_ldec_cnv (h) (a) (G) (K):
-      ∀W. ❪G,K❫ ⊢ W ![h,a] →
-      ∀U. ⇧*[1] W ≘ U → ❪G,K.ⓛW❫ ⊢ #0 :[h,a] U.
+      ∀W. ❨G,K❩ ⊢ W ![h,a] →
+      ∀U. ⇧[1] W ≘ U → ❨G,K.ⓛW❩ ⊢ #0 :[h,a] U.
 #h #a #G #K #W #HW #U #HWU
 lapply (cnv_lifts … HW (Ⓣ) … (K.ⓛW) … HWU)
 /3 width=5 by cnv_zero, cnv_cast, cpms_ell, drops_refl, drops_drop/
 qed.
 
 lemma nta_lref (h) (a) (I) (G) (K):
-      ∀T,i. ❪G,K❫ ⊢ #i :[h,a] T →
-      ∀U. ⇧*[1] T ≘ U → ❪G,K.ⓘ[I]❫ ⊢ #(↑i) :[h,a] U.
+      ∀T,i. ❨G,K❩ ⊢ #i :[h,a] T →
+      ∀U. ⇧[1] T ≘ U → ❨G,K.ⓘ[I]❩ ⊢ #(↑i) :[h,a] U.
 #h #a #I #G #K #T #i #H #U #HTU
 elim (cnv_inv_cast … H) -H #X #HT #Hi #HTX #H2
 lapply (cnv_lifts … HT (Ⓣ) … (K.ⓘ[I]) … HTU) -HT
@@ -75,16 +75,16 @@ lemma nta_lifts_bi (h) (a) (G): d_liftable2_bi … lifts (nta a h G).
 (* Basic_1: was by definition: ty3_abbr *)
 (* Basic_2A1: was by definition: nta_ldef ntaa_ldef *)
 lemma nta_ldef_drops (h) (a) (G) (K) (L) (i):
-      ∀V,W. ❪G,K❫ ⊢ V :[h,a] W →
-      ∀U. ⇧*[↑i] W ≘ U → ⇩*[i] L ≘ K.ⓓV → ❪G,L❫ ⊢ #i :[h,a] U.
+      ∀V,W. ❨G,K❩ ⊢ V :[h,a] W →
+      ∀U. ⇧[↑i] W ≘ U → ⇩[i] L ≘ K.ⓓV → ❨G,L❩ ⊢ #i :[h,a] U.
 #h #a #G #K #L #i #V #W #HVW #U #HWU #HLK
 elim (lifts_split_trans … HWU (𝐔❨1❩) (𝐔❨i❩)) [| // ] #X #HWX #HXU
 /3 width=9 by nta_lifts_bi, nta_ldef/
 qed.
 
 lemma nta_ldec_drops_cnv (h) (a) (G) (K) (L) (i):
-      ∀W. ❪G,K❫ ⊢ W ![h,a] →
-      ∀U. ⇧*[↑i] W ≘ U → ⇩*[i] L ≘ K.ⓛW → ❪G,L❫ ⊢ #i :[h,a] U.
+      ∀W. ❨G,K❩ ⊢ W ![h,a] →
+      ∀U. ⇧[↑i] W ≘ U → ⇩[i] L ≘ K.ⓛW → ❨G,L❩ ⊢ #i :[h,a] U.
 #h #a #G #K #L #i #W #HW #U #HWU #HLK
 elim (lifts_split_trans … HWU (𝐔❨1❩) (𝐔❨i❩)) [| // ] #X #HWX #HXU
 /3 width=9 by nta_lifts_bi, nta_ldec_cnv/