milestone in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / nta.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
index 8f6e4c6be9190e0399e7f2884aea92eb2219f947..66ddc0d99cedabd61df19e96ec724ff12ba811a4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
@@ -26,10 +26,10 @@ 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 true h G L T U).
+   '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 false h G L T U).
+   'ColonStar h G L T U = (nta Y h G L T U).
 
 (* Basic properties *********************************************************)
 
@@ -66,6 +66,15 @@ elim (cnv_inv_cast … H2) #X2 #_ #_ #HTX2 #HTX12
 /3 width=3 by cnv_cast, cpms_eps/
 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
+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):
@@ -81,54 +90,6 @@ lemma nta_fwd_cnv_dx (a) (h) (G) (L):
 elim (cnv_inv_cast … H) -H #X #HU #_ #_ #_ //
 qed-.
 
-(*
-
-| nta_ldef: ∀L,K,V,W,U,i. ⇩[0, i] L ≡ K. ⓓV → nta h K V W →
-            ⇧[0, i + 1] W ≡ U → nta h L (#i) U
-| nta_ldec: ∀L,K,W,V,U,i. ⇩[0, i] L ≡ K. ⓛW → nta h K W V →
-            ⇧[0, i + 1] W ≡ U → nta h L (#i) U
-.
-
-(* Basic properties *********************************************************)
-
-lemma nta_ind_alt: ∀h. ∀R:lenv→relation term.
-   (∀L,k. R L ⋆k ⋆(next h k)) →
-   (∀L,K,V,W,U,i.
-      ⇩[O, i] L ≡ K.ⓓV → ⦃h, K⦄ ⊢ V : W → ⇧[O, i + 1] W ≡ U →
-      R K V W → R L (#i) U 
-   ) →
-   (∀L,K,W,V,U,i.
-      ⇩[O, i] L ≡ K.ⓛW → ⦃h, K⦄ ⊢ W : V → ⇧[O, i + 1] W ≡ U →
-      R K W V → R L (#i) U
-   ) →
-   (∀I,L,V,W,T,U.
-      ⦃h, L⦄ ⊢ V : W → ⦃h, L.ⓑ{I}V⦄ ⊢ T : U →
-      R L V W → R (L.ⓑ{I}V) T U → R L (ⓑ{I}V.T) (ⓑ{I}V.U)
-   ) →
-   (∀L,V,W,T,U.
-      ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ (ⓛW.T):(ⓛW.U) →
-      R L V W →R L (ⓛW.T) (ⓛW.U) →R L (ⓐV.ⓛW.T) (ⓐV.ⓛW.U)
-   ) →
-   (∀L,V,W,T,U.
-      ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ (ⓐV.U) : W →
-      R L T U → R L (ⓐV.U) W → R L (ⓐV.T) (ⓐV.U)
-   ) →
-   (∀L,T,U,W.
-      ⦃h, L⦄ ⊢ T : U → ⦃h, L⦄ ⊢ U : W →
-      R L T U → R L U W → R L (ⓝU.T) U
-   ) →
-   (∀L,T,U1,U2,V2.
-      ⦃h, L⦄ ⊢ T : U1 → L ⊢ U1 ⬌* U2 → ⦃h, L⦄ ⊢ U2 : V2 →
-      R L T U1 →R L U2 V2 →R L T U2
-   ) →
-   ∀L,T,U. ⦃h, L⦄ ⊢ T : U → R L T U.
-#h #R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #L #T #U #H elim (nta_ntaa … H) -L -T -U
-// /3 width=1 by ntaa_nta/ /3 width=3 by ntaa_nta/ /3 width=4 by ntaa_nta/
-/3 width=7 by ntaa_nta/
-qed-.
-
-*)
-
 (* Basic_1: removed theorems 4:
             ty3_getl_subst0 ty3_fsubst0 ty3_csubst0 ty3_subst0
 *)