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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma
index c0d2b0cf1..7f74c5f06 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.ma
@@ -18,7 +18,7 @@ include "basic_2/dynamic/cnv.ma".
 (* ITERATED NATIVE TYPE ASSIGNMENT FOR TERMS ********************************)
 
 definition ntas (h) (a) (n) (G) (L): relation term ≝ λT,U.
-           ∃∃U0. ⦃G,L⦄ ⊢ U ![h,a] & ⦃G,L⦄ ⊢ T ![h,a] & ⦃G,L⦄ ⊢ U ➡*[h] U0 & ⦃G,L⦄ ⊢ T ➡*[n,h] U0.
+           ∃∃U0. ❪G,L❫ ⊢ U ![h,a] & ❪G,L❫ ⊢ T ![h,a] & ❪G,L❫ ⊢ U ➡*[h] U0 & ❪G,L❫ ⊢ T ➡*[n,h] U0.
 
 interpretation "iterated native type assignment (term)"
    'ColonStar h a n G L T U = (ntas h a n G L T U).
@@ -26,24 +26,24 @@ interpretation "iterated native type assignment (term)"
 (* Basic properties *********************************************************)
 
 lemma ntas_intro (h) (a) (n) (G) (L):
-      ∀U. ⦃G,L⦄ ⊢ U ![h,a] → ∀T. ⦃G,L⦄ ⊢ T ![h,a] →
-      ∀U0. ⦃G,L⦄ ⊢ U ➡*[h] U0 → ⦃G,L⦄ ⊢ T ➡*[n,h] U0 → ⦃G,L⦄ ⊢ T :*[h,a,n] U.
+      ∀U. ❪G,L❫ ⊢ U ![h,a] → ∀T. ❪G,L❫ ⊢ T ![h,a] →
+      ∀U0. ❪G,L❫ ⊢ U ➡*[h] U0 → ❪G,L❫ ⊢ T ➡*[n,h] U0 → ❪G,L❫ ⊢ T :*[h,a,n] U.
 /2 width=3 by ex4_intro/ qed.
 
 lemma ntas_refl (h) (a) (G) (L):
-      ∀T. ⦃G,L⦄ ⊢ T ![h,a] → ⦃G,L⦄ ⊢ T :*[h,a,0] T.
+      ∀T. ❪G,L❫ ⊢ T ![h,a] → ❪G,L❫ ⊢ T :*[h,a,0] T.
 /2 width=3 by ntas_intro/ qed.
 
 lemma ntas_sort (h) (a) (n) (G) (L):
-      ∀s. ⦃G,L⦄ ⊢ ⋆s :*[h,a,n] ⋆((next h)^n s).
+      ∀s. ❪G,L❫ ⊢ ⋆s :*[h,a,n] ⋆((next h)^n s).
 #h #a #n #G #L #s
 /2 width=3 by ntas_intro, cnv_sort, cpms_sort/
 qed.
 
 lemma ntas_bind_cnv (h) (a) (n) (G) (K):
-      ∀V. ⦃G,K⦄ ⊢ V ![h,a] →
-      ∀I,T,U. ⦃G,K.ⓑ{I}V⦄ ⊢ T :*[h,a,n] U →
-      ∀p. ⦃G,K⦄ ⊢ ⓑ{p,I}V.T :*[h,a,n] ⓑ{p,I}V.U.
+      ∀V. ❪G,K❫ ⊢ V ![h,a] →
+      ∀I,T,U. ❪G,K.ⓑ[I]V❫ ⊢ T :*[h,a,n] U →
+      ∀p. ❪G,K❫ ⊢ ⓑ[p,I]V.T :*[h,a,n] ⓑ[p,I]V.U.
 #h #a #n #G #K #V #HV #I #T #U
 * #X #HU #HT #HUX #HTX #p
 /3 width=5 by ntas_intro, cnv_bind, cpms_bind_dx/
@@ -52,14 +52,14 @@ qed.
 (* Basic_forward lemmas *****************************************************)
 
 lemma ntas_fwd_cnv_sn (h) (a) (n) (G) (L):
-      ∀T,U. ⦃G,L⦄ ⊢ T :*[h,a,n] U → ⦃G,L⦄ ⊢ T ![h,a].
+      ∀T,U. ❪G,L❫ ⊢ T :*[h,a,n] U → ❪G,L❫ ⊢ T ![h,a].
 #h #a #n #G #L #T #U
 * #X #_ #HT #_ #_ //
 qed-.
 
 (* Note: this is ntas_fwd_correct_cnv *)
 lemma ntas_fwd_cnv_dx (h) (a) (n) (G) (L):
-      ∀T,U. ⦃G,L⦄ ⊢ T :*[h,a,n] U → ⦃G,L⦄ ⊢ U ![h,a].
+      ∀T,U. ❪G,L❫ ⊢ T :*[h,a,n] U → ❪G,L❫ ⊢ U ![h,a].
 #h #a #n #G #L #T #U
 * #X #HU #_ #_ #_ //
 qed-.