update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / i_dynamic / ntas_nta.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta.ma b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta.ma
index c7fd9cb2637164bc369c60ae17393c77e476a801..409f06b81407fdfc6f32741c21f7fe36b12e6ff9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_nta.ma
@@ -20,12 +20,12 @@ include "basic_2/i_dynamic/ntas_preserve.ma".
 (* Advanced properties of native validity for terms *************************)
 
 lemma cnv_appl_ntas_ge (h) (a) (G) (L):
-      â\88\80m,n. m â\89¤ n â\86\92 ad a n â\86\92 â\88\80V,W. â¦\83G,Lâ¦\84 ⊢ V :[h,a] W →
-      â\88\80p,T,U. â¦\83G,Lâ¦\84 â\8a¢ T :*[h,a,m] â\93\9b{p}W.U â\86\92 â¦\83G,Lâ¦\84 ⊢ ⓐV.T ![h,a].
+      â\88\80m,n. m â\89¤ n â\86\92 ad a n â\86\92 â\88\80V,W. â\9dªG,Lâ\9d« ⊢ V :[h,a] W →
+      â\88\80p,T,U. â\9dªG,Lâ\9d« â\8a¢ T :*[h,a,m] â\93\9b[p]W.U â\86\92 â\9dªG,Lâ\9d« ⊢ ⓐV.T ![h,a].
 #h #a #G #L #m #n #Hmn #Hn #V #W #HVW #p #T #U #HTU
 elim (cnv_inv_cast … HVW) -HVW #W0 #HW #HV #HW0 #HVW0
 elim HTU -HTU #U0 #H #HT #HU0 #HTU0
-elim (cnv_cpms_conf … H … HU0 0 (ⓛ{p}W0.U)) -H -HU0
+elim (cnv_cpms_conf … H … HU0 0 (ⓛ[p]W0.U)) -H -HU0
 [| /2 width=1 by cpms_bind/ ] -HW0 <minus_n_O #X0 #HUX0 #H
 elim (cpms_inv_abst_sn … H) -H #W1 #U1 #HW01 #_ #H destruct
 /3 width=13 by cnv_appl_ge, cpms_cprs_trans/
@@ -34,8 +34,8 @@ qed-.
 (* Advanced inversion lemmas of native validity for terms *******************)
 
 lemma cnv_inv_appl_ntas (h) (a) (G) (L):
-      â\88\80V,T. â¦\83G,Lâ¦\84 ⊢ ⓐV.T ![h,a] →
-      â\88\83â\88\83n,p,W,T,U. ad a n & â¦\83G,Lâ¦\84 â\8a¢ V :[h,a] W & â¦\83G,Lâ¦\84 â\8a¢ T :*[h,a,n] â\93\9b{p}W.U.
+      â\88\80V,T. â\9dªG,Lâ\9d« ⊢ ⓐV.T ![h,a] →
+      â\88\83â\88\83n,p,W,T,U. ad a n & â\9dªG,Lâ\9d« â\8a¢ V :[h,a] W & â\9dªG,Lâ\9d« â\8a¢ T :*[h,a,n] â\93\9b[p]W.U.
 #h #a #G #L #V #T #H
 elim (cnv_inv_appl … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
 /3 width=9 by cnv_cpms_nta, cnv_cpms_ntas, ex3_5_intro/
@@ -44,14 +44,14 @@ qed-.
 (* Properties with native type assignment for terms *************************)
 
 lemma nta_ntas (h) (a) (G) (L):
-      â\88\80T,U. â¦\83G,Lâ¦\84 â\8a¢ T :[h,a] U â\86\92 â¦\83G,Lâ¦\84 ⊢ T :*[h,a,1] U.
+      â\88\80T,U. â\9dªG,Lâ\9d« â\8a¢ T :[h,a] U â\86\92 â\9dªG,Lâ\9d« ⊢ T :*[h,a,1] U.
 #h #a #G #L #T #U #H
 elim (cnv_inv_cast … H) -H /2 width=3 by ntas_intro/
 qed-.
 
 lemma ntas_step_sn (h) (a) (G) (L):
-      â\88\80T1,T. â¦\83G,Lâ¦\84 ⊢ T1 :[h,a] T →
-      â\88\80n,T2. â¦\83G,Lâ¦\84 â\8a¢ T :*[h,a,n] T2 â\86\92 â¦\83G,Lâ¦\84 ⊢ T1 :*[h,a,↑n] T2.
+      â\88\80T1,T. â\9dªG,Lâ\9d« ⊢ T1 :[h,a] T →
+      â\88\80n,T2. â\9dªG,Lâ\9d« â\8a¢ T :*[h,a,n] T2 â\86\92 â\9dªG,Lâ\9d« ⊢ T1 :*[h,a,↑n] T2.
 #h #a #G #L #T1 #T #H #n #T2 * #X2 #HT2 #HT #H1TX2 #H2TX2
 elim (cnv_inv_cast … H) -H #X1 #_ #HT1 #H1TX1 #H2TX1
 elim (cnv_cpms_conf … HT … H1TX1 … H2TX2) -T <minus_n_O <minus_O_n <plus_SO_sn #X #HX1 #HX2
@@ -59,8 +59,8 @@ elim (cnv_cpms_conf … HT … H1TX1 … H2TX2) -T <minus_n_O <minus_O_n <plus_S
 qed-.
 
 lemma ntas_step_dx (h) (a) (G) (L):
-      â\88\80n,T1,T. â¦\83G,Lâ¦\84 ⊢ T1 :*[h,a,n] T →
-      â\88\80T2. â¦\83G,Lâ¦\84 â\8a¢ T :[h,a] T2 â\86\92 â¦\83G,Lâ¦\84 ⊢ T1 :*[h,a,↑n] T2.
+      â\88\80n,T1,T. â\9dªG,Lâ\9d« ⊢ T1 :*[h,a,n] T →
+      â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T :[h,a] T2 â\86\92 â\9dªG,Lâ\9d« ⊢ T1 :*[h,a,↑n] T2.
 #h #a #G #L #n #T1 #T * #X1 #HT #HT1 #H1TX1 #H2TX1 #T2 #H
 elim (cnv_inv_cast … H) -H #X2 #HT2 #_ #H1TX2 #H2TX2
 elim (cnv_cpms_conf … HT … H1TX1 … H2TX2) -T <minus_n_O <minus_O_n <plus_SO_dx #X #HX1 #HX2
@@ -68,8 +68,8 @@ elim (cnv_cpms_conf … HT … H1TX1 … H2TX2) -T <minus_n_O <minus_O_n <plus_S
 qed-.
 
 lemma nta_appl_ntas_zero (h) (a) (G) (L): ad a 0 →
-      â\88\80V,W. â¦\83G,Lâ¦\84 â\8a¢ V :[h,a] W â\86\92 â\88\80p,T,U0. â¦\83G,Lâ¦\84 â\8a¢ T :*[h,a,0] â\93\9b{p}W.U0 →
-      â\88\80U. â¦\83G,L.â\93\9bWâ¦\84 â\8a¢ U0 :[h,a] U â\86\92 â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.T :[h,a] â\93\90V.â\93\9b{p}W.U.
+      â\88\80V,W. â\9dªG,Lâ\9d« â\8a¢ V :[h,a] W â\86\92 â\88\80p,T,U0. â\9dªG,Lâ\9d« â\8a¢ T :*[h,a,0] â\93\9b[p]W.U0 →
+      â\88\80U. â\9dªG,L.â\93\9bWâ\9d« â\8a¢ U0 :[h,a] U â\86\92 â\9dªG,Lâ\9d« â\8a¢ â\93\90V.T :[h,a] â\93\90V.â\93\9b[p]W.U.
 #h #a #G #L #Ha #V #W #HVW #p #T #U0 #HTU0 #U #HU0
 lapply (nta_fwd_cnv_dx … HVW) #HW
 lapply (nta_bind_cnv … HW … HU0 p) -HW -HU0 #HU0
@@ -78,8 +78,8 @@ elim (ntas_step_dx … HTU0 … HU0) -HU0 #X #HU #_ #HUX #HTX
 qed.
 
 lemma nta_appl_ntas_pos (h) (a) (n) (G) (L): ad a (↑n) →
-      â\88\80V,W. â¦\83G,Lâ¦\84 â\8a¢ V :[h,a] W â\86\92 â\88\80T,U. â¦\83G,Lâ¦\84 ⊢ T :[h,a] U →
-      â\88\80p,U0. â¦\83G,Lâ¦\84 â\8a¢ U :*[h,a,n] â\93\9b{p}W.U0 â\86\92 â¦\83G,Lâ¦\84 ⊢ ⓐV.T :[h,a] ⓐV.U.
+      â\88\80V,W. â\9dªG,Lâ\9d« â\8a¢ V :[h,a] W â\86\92 â\88\80T,U. â\9dªG,Lâ\9d« ⊢ T :[h,a] U →
+      â\88\80p,U0. â\9dªG,Lâ\9d« â\8a¢ U :*[h,a,n] â\93\9b[p]W.U0 â\86\92 â\9dªG,Lâ\9d« ⊢ ⓐV.T :[h,a] ⓐV.U.
 #h #a #n #G #L #Ha #V #W #HVW #T #U #HTU #p #U0 #HU0
 elim (cnv_inv_cast … HTU) #X #_ #_ #HUX #HTX
 /4 width=11 by ntas_step_sn, cnv_appl_ntas_ge, cnv_cast, cpms_appl_dx/
@@ -88,16 +88,16 @@ qed-.
 (* Inversion lemmas with native type assignment for terms *******************)
 
 lemma ntas_inv_nta (h) (a) (G) (L):
-      â\88\80T,U. â¦\83G,Lâ¦\84 â\8a¢ T :*[h,a,1] U â\86\92 â¦\83G,Lâ¦\84 ⊢ T :[h,a] U.
+      â\88\80T,U. â\9dªG,Lâ\9d« â\8a¢ T :*[h,a,1] U â\86\92 â\9dªG,Lâ\9d« ⊢ T :[h,a] U.
 #h #a #G #L #T #U
 * /2 width=3 by cnv_cast/
 qed-.
 
 (* Note: this follows from ntas_inv_appl_sn *)
 lemma nta_inv_appl_sn_ntas (h) (a) (G) (L) (V) (T):
-      â\88\80X. â¦\83G,Lâ¦\84 ⊢ ⓐV.T :[h,a] X →
-      â\88¨â\88¨ â\88\83â\88\83p,W,U,U0. ad a 0 & â¦\83G,Lâ¦\84 â\8a¢ V :[h,a] W & â¦\83G,Lâ¦\84 â\8a¢ T :*[h,a,0] â\93\9b{p}W.U0 & â¦\83G,L.â\93\9bWâ¦\84 â\8a¢ U0 :[h,a] U & â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.â\93\9b{p}W.U â¬\8c*[h] X & â¦\83G,Lâ¦\84 ⊢ X ![h,a]
-       | â\88\83â\88\83n,p,W,U,U0. ad a (â\86\91n) & â¦\83G,Lâ¦\84 â\8a¢ V :[h,a] W & â¦\83G,Lâ¦\84 â\8a¢ T :[h,a] U & â¦\83G,Lâ¦\84 â\8a¢ U :*[h,a,n] â\93\9b{p}W.U0 & â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.U â¬\8c*[h] X & â¦\83G,Lâ¦\84 ⊢ X ![h,a].
+      â\88\80X. â\9dªG,Lâ\9d« ⊢ ⓐV.T :[h,a] X →
+      â\88¨â\88¨ â\88\83â\88\83p,W,U,U0. ad a 0 & â\9dªG,Lâ\9d« â\8a¢ V :[h,a] W & â\9dªG,Lâ\9d« â\8a¢ T :*[h,a,0] â\93\9b[p]W.U0 & â\9dªG,L.â\93\9bWâ\9d« â\8a¢ U0 :[h,a] U & â\9dªG,Lâ\9d« â\8a¢ â\93\90V.â\93\9b[p]W.U â¬\8c*[h] X & â\9dªG,Lâ\9d« ⊢ X ![h,a]
+       | â\88\83â\88\83n,p,W,U,U0. ad a (â\86\91n) & â\9dªG,Lâ\9d« â\8a¢ V :[h,a] W & â\9dªG,Lâ\9d« â\8a¢ T :[h,a] U & â\9dªG,Lâ\9d« â\8a¢ U :*[h,a,n] â\93\9b[p]W.U0 & â\9dªG,Lâ\9d« â\8a¢ â\93\90V.U â¬\8c*[h] X & â\9dªG,Lâ\9d« ⊢ X ![h,a].
 #h #a #G #L #V #T #X #H
 (* Note: insert here: alternate proof in ntas_nta.etc *)
 elim (cnv_inv_cast … H) -H #X0 #HX #HVT #HX0 #HTX0