X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fnta.ma;h=690e7d66800da402cc27e3d313ea790bd4ea2eae;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hp=66ddc0d99cedabd61df19e96ec724ff12ba811a4;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
index 66ddc0d99..690e7d668 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
@@ -13,54 +13,46 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/colon_6.ma".
-include "basic_2/notation/relations/colon_5.ma".
-include "basic_2/notation/relations/colonstar_5.ma".
 include "basic_2/dynamic/cnv.ma".
 
 (* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
 
-definition nta (a) (h): relation4 genv lenv term term ≝
-                        λG,L,T,U. ⦃G,L⦄ ⊢ ⓝU.T ![a,h].
+definition nta (h) (a): relation4 genv lenv term term ≝
+           λG,L,T,U. ❪G,L❫ ⊢ ⓝU.T ![h,a].
 
 interpretation "native type assignment (term)"
-   'Colon a h G L T U = (nta a h G L T U).
-
-interpretation "restricted native type assignment (term)"
-   'Colon h G L T U = (nta (yinj (S (S O))) h G L T U).
-
-interpretation "extended native type assignment (term)"
-   'ColonStar h G L T U = (nta Y h G L T U).
+  'Colon h a G L T U = (nta h a G L T U).
 
 (* Basic properties *********************************************************)
 
 (* Basic_1: was by definition: ty3_sort *)
 (* Basic_2A1: was by definition: nta_sort ntaa_sort *)
-lemma nta_sort (a) (h) (G) (L) (s): ⦃G,L⦄ ⊢ ⋆s :[a,h] ⋆(next h s).
-#a #h #G #L #s /2 width=3 by cnv_sort, cnv_cast, cpms_sort/
+lemma nta_sort (h) (a) (G) (L): ∀s. ❪G,L❫ ⊢ ⋆s :[h,a] ⋆(⫯[h]s).
+#h #a #G #L #s /2 width=3 by cnv_sort, cnv_cast, cpms_sort/
 qed.
 
-lemma nta_bind_cnv (a) (h) (G) (K):
-      ∀V. ⦃G,K⦄ ⊢ V ![a,h] →
-      ∀I,T,U. ⦃G,K.ⓑ{I}V⦄ ⊢ T :[a,h] U →
-      ∀p. ⦃G,K⦄ ⊢ ⓑ{p,I}V.T :[a,h] ⓑ{p,I}V.U.
-#a #h #G #K #V #HV #I #T #U #H #p
+lemma nta_bind_cnv (h) (a) (G) (K):
+      ∀V. ❪G,K❫ ⊢ V ![h,a] →
+      ∀I,T,U. ❪G,K.ⓑ[I]V❫ ⊢ T :[h,a] U →
+      ∀p. ❪G,K❫ ⊢ ⓑ[p,I]V.T :[h,a] ⓑ[p,I]V.U.
+#h #a #G #K #V #HV #I #T #U #H #p
 elim (cnv_inv_cast … H) -H #X #HU #HT #HUX #HTX
 /3 width=5 by cnv_bind, cnv_cast, cpms_bind_dx/
 qed.
 
 (* Basic_2A1: was by definition: nta_cast *)
-lemma nta_cast (a) (h) (G) (L):
-      ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ ⓝU.T :[a,h] U.
-#a #h #G #L #T #U #H
+lemma nta_cast (h) (a) (G) (L):
+      ∀T,U. ❪G,L❫ ⊢ T :[h,a] U → ❪G,L❫ ⊢ ⓝU.T :[h,a] U.
+#h #a #G #L #T #U #H
 elim (cnv_inv_cast … H) #X #HU #HT #HUX #HTX
 /3 width=3 by cnv_cast, cpms_eps/
 qed.
 
 (* Basic_1: was by definition: ty3_cast *)
-lemma nta_cast_old (a) (h) (G) (L):
-      ∀T0,T1. ⦃G,L⦄ ⊢ T0 :[a,h] T1 →
-      ∀T2. ⦃G,L⦄ ⊢ T1 :[a,h] T2 → ⦃G,L⦄ ⊢ ⓝT1.T0 :[a,h] ⓝT2.T1.
-#a #h #G #L #T0 #T1 #H1 #T2 #H2
+lemma nta_cast_old (h) (a) (G) (L):
+      ∀T0,T1. ❪G,L❫ ⊢ T0 :[h,a] T1 →
+      ∀T2. ❪G,L❫ ⊢ T1 :[h,a] T2 → ❪G,L❫ ⊢ ⓝT1.T0 :[h,a] ⓝT2.T1.
+#h #a #G #L #T0 #T1 #H1 #T2 #H2
 elim (cnv_inv_cast … H1) #X1 #_ #_ #HTX1 #HTX01
 elim (cnv_inv_cast … H2) #X2 #_ #_ #HTX2 #HTX12
 /3 width=3 by cnv_cast, cpms_eps/
@@ -68,25 +60,25 @@ qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma nta_inv_gref_sn (a) (h) (G) (L):
-      ∀X2,l. ⦃G,L⦄ ⊢ §l :[a,h] X2 → ⊥.
-#a #h #G #L #X2 #l #H
+lemma nta_inv_gref_sn (h) (a) (G) (L):
+      ∀X2,l. ❪G,L❫ ⊢ §l :[h,a] X2 → ⊥.
+#h #a #G #L #X2 #l #H
 elim (cnv_inv_cast … H) -H #X #_ #H #_ #_
 elim (cnv_inv_gref … H)
 qed-.
 
 (* Basic_forward lemmas *****************************************************)
 
-lemma nta_fwd_cnv_sn (a) (h) (G) (L):
-                     ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ T ![a,h].
-#a #h #G #L #T #U #H
+lemma nta_fwd_cnv_sn (h) (a) (G) (L):
+      ∀T,U. ❪G,L❫ ⊢ T :[h,a] U → ❪G,L❫ ⊢ T ![h,a].
+#h #a #G #L #T #U #H
 elim (cnv_inv_cast … H) -H #X #_ #HT #_ #_ //
 qed-.
 
 (* Note: this is nta_fwd_correct_cnv *)
-lemma nta_fwd_cnv_dx (a) (h) (G) (L):
-                     ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ U ![a,h].
-#a #h #G #L #T #U #H
+lemma nta_fwd_cnv_dx (h) (a) (G) (L):
+      ∀T,U. ❪G,L❫ ⊢ T :[h,a] U → ❪G,L❫ ⊢ U ![h,a].
+#h #a #G #L #T #U #H
 elim (cnv_inv_cast … H) -H #X #HU #_ #_ #_ //
 qed-.