update in ground static_2 basic_2 apps_2

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

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 8db13303581a45042b68cb06a76d4bab24265ad6..059fe374fc9e88d75835cb505f7db2d961789764 100644 (file)
--- 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.
-           â\88\83â\88\83U0. â\9dªG,Lâ\9d« â\8a¢ U ![h,a] & â\9dªG,Lâ\9d« â\8a¢ T ![h,a] & â\9dªG,Lâ\9d« â\8a¢ U â\9e¡*[h,0] U0 & â\9dªG,Lâ\9d« ⊢ T ➡*[h,n] U0.
+           â\88\83â\88\83U0. â\9d¨G,Lâ\9d© â\8a¢ U ![h,a] & â\9d¨G,Lâ\9d© â\8a¢ T ![h,a] & â\9d¨G,Lâ\9d© â\8a¢ U â\9e¡*[h,0] U0 & â\9d¨G,Lâ\9d© ⊢ T ➡*[h,n] 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):
-      â\88\80U. â\9dªG,Lâ\9d« â\8a¢ U ![h,a] â\86\92 â\88\80T. â\9dªG,Lâ\9d« ⊢ T ![h,a] →
-      â\88\80U0. â\9dªG,Lâ\9d« â\8a¢ U â\9e¡*[h,0] U0 â\86\92 â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[h,n] U0 â\86\92 â\9dªG,Lâ\9d« ⊢ T :*[h,a,n] U.
+      â\88\80U. â\9d¨G,Lâ\9d© â\8a¢ U ![h,a] â\86\92 â\88\80T. â\9d¨G,Lâ\9d© ⊢ T ![h,a] →
+      â\88\80U0. â\9d¨G,Lâ\9d© â\8a¢ U â\9e¡*[h,0] U0 â\86\92 â\9d¨G,Lâ\9d© â\8a¢ T â\9e¡*[h,n] U0 â\86\92 â\9d¨G,Lâ\9d© ⊢ T :*[h,a,n] U.
 /2 width=3 by ex4_intro/ qed.
 
 lemma ntas_refl (h) (a) (G) (L):
-      â\88\80T. â\9dªG,Lâ\9d« â\8a¢ T ![h,a] â\86\92 â\9dªG,Lâ\9d« ⊢ T :*[h,a,0] T.
+      â\88\80T. â\9d¨G,Lâ\9d© â\8a¢ T ![h,a] â\86\92 â\9d¨G,Lâ\9d© ⊢ T :*[h,a,0] T.
 /2 width=3 by ntas_intro/ qed.
 
 lemma ntas_sort (h) (a) (n) (G) (L):
-      â\88\80s. â\9dªG,Lâ\9d« ⊢ ⋆s :*[h,a,n] ⋆((next h)^n s).
+      â\88\80s. â\9d¨G,Lâ\9d© ⊢ ⋆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):
-      â\88\80V. â\9dªG,Kâ\9d« ⊢ V ![h,a] →
-      â\88\80I,T,U. â\9dªG,K.â\93\91[I]Vâ\9d« ⊢ T :*[h,a,n] U →
-      â\88\80p. â\9dªG,Kâ\9d« ⊢ ⓑ[p,I]V.T :*[h,a,n] ⓑ[p,I]V.U.
+      â\88\80V. â\9d¨G,Kâ\9d© ⊢ V ![h,a] →
+      â\88\80I,T,U. â\9d¨G,K.â\93\91[I]Vâ\9d© ⊢ T :*[h,a,n] U →
+      â\88\80p. â\9d¨G,Kâ\9d© ⊢ ⓑ[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):
-      â\88\80T,U. â\9dªG,Lâ\9d« â\8a¢ T :*[h,a,n] U â\86\92 â\9dªG,Lâ\9d« ⊢ T ![h,a].
+      â\88\80T,U. â\9d¨G,Lâ\9d© â\8a¢ T :*[h,a,n] U â\86\92 â\9d¨G,Lâ\9d© ⊢ 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):
-      â\88\80T,U. â\9dªG,Lâ\9d« â\8a¢ T :*[h,a,n] U â\86\92 â\9dªG,Lâ\9d« ⊢ U ![h,a].
+      â\88\80T,U. â\9d¨G,Lâ\9d© â\8a¢ T :*[h,a,n] U â\86\92 â\9d¨G,Lâ\9d© ⊢ U ![h,a].
 #h #a #n #G #L #T #U
 * #X #HU #_ #_ #_ //
 qed-.