updating the structures for sorts

[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 1942111912c46ec091dfb750c19f8f4977e4708a..84bbfeda94a2c4df1493e9833e525707ee2134a7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.ma
@@ -26,16 +26,16 @@ 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 *********************************************************)
 
 (* 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).
+lemma nta_sort (a) (h) (G) (L) (s): ⦃G,L⦄ ⊢ ⋆s :[a,h] ⋆(⫯[h]s).
 #a #h #G #L #s /2 width=3 by cnv_sort, cnv_cast, cpms_sort/
 qed.
 
@@ -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):