update in ground_2, static_2, basic_2, apps_2, alpha_1

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

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
index 14da27905e1dadb6a30b6719580c579550a28f73..256b798b50a2c1694874654586e618844e95aa22 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
@@ -23,13 +23,13 @@ include "basic_2/rt_computation/cpms.ma".
 (* Basic_2A1: uses: snv *)
 inductive cnv (h) (a): relation3 genv lenv term ≝
 | cnv_sort: ∀G,L,s. cnv h a G L (⋆s)
-| cnv_zero: ∀I,G,K,V. cnv h a G K V → cnv h a G (K.ⓑ{I}V) (#0)
-| cnv_lref: ∀I,G,K,i. cnv h a G K (#i) → cnv h a G (K.ⓘ{I}) (#↑i)
-| cnv_bind: ∀p,I,G,L,V,T. cnv h a G L V → cnv h a G (L.ⓑ{I}V) T → cnv h a G L (ⓑ{p,I}V.T)
+| cnv_zero: ∀I,G,K,V. cnv h a G K V → cnv h a G (K.ⓑ[I]V) (#0)
+| cnv_lref: ∀I,G,K,i. cnv h a G K (#i) → cnv h a G (K.ⓘ[I]) (#↑i)
+| cnv_bind: ∀p,I,G,L,V,T. cnv h a G L V → cnv h a G (L.ⓑ[I]V) T → cnv h a G L (ⓑ[p,I]V.T)
 | cnv_appl: ∀n,p,G,L,V,W0,T,U0. ad a n → cnv h a G L V → cnv h a G L T →
-            â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡*[1,h] W0 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] â\93\9b{p}W0.U0 → cnv h a G L (ⓐV.T)
+            â\9dªG,Lâ\9d« â\8a¢ V â\9e¡*[1,h] W0 â\86\92 â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[n,h] â\93\9b[p]W0.U0 → cnv h a G L (ⓐV.T)
 | cnv_cast: ∀G,L,U,T,U0. cnv h a G L U → cnv h a G L T →
-            â¦\83G,Lâ¦\84 â\8a¢ U â\9e¡*[h] U0 â\86\92 â¦\83G,Lâ¦\84 ⊢ T ➡*[1,h] U0 → cnv h a G L (ⓝU.T)
+            â\9dªG,Lâ\9d« â\8a¢ U â\9e¡*[h] U0 â\86\92 â\9dªG,Lâ\9d« ⊢ T ➡*[1,h] U0 → cnv h a G L (ⓝU.T)
 .
 
 interpretation "context-sensitive native validity (term)"
@@ -38,8 +38,8 @@ interpretation "context-sensitive native validity (term)"
 (* Basic inversion lemmas ***************************************************)
 
 fact cnv_inv_zero_aux (h) (a):
-     â\88\80G,L,X. â¦\83G,Lâ¦\84 ⊢ X ![h,a] → X = #0 →
-     â\88\83â\88\83I,K,V. â¦\83G,Kâ¦\84 â\8a¢ V ![h,a] & L = K.â\93\91{I}V.
+     â\88\80G,L,X. â\9dªG,Lâ\9d« ⊢ X ![h,a] → X = #0 →
+     â\88\83â\88\83I,K,V. â\9dªG,Kâ\9d« â\8a¢ V ![h,a] & L = K.â\93\91[I]V.
 #h #a #G #L #X * -G -L -X
 [ #G #L #s #H destruct
 | #I #G #K #V #HV #_ /2 width=5 by ex2_3_intro/
@@ -51,13 +51,13 @@ fact cnv_inv_zero_aux (h) (a):
 qed-.
 
 lemma cnv_inv_zero (h) (a):
-      â\88\80G,L. â¦\83G,Lâ¦\84 ⊢ #0 ![h,a] →
-      â\88\83â\88\83I,K,V. â¦\83G,Kâ¦\84 â\8a¢ V ![h,a] & L = K.â\93\91{I}V.
+      â\88\80G,L. â\9dªG,Lâ\9d« ⊢ #0 ![h,a] →
+      â\88\83â\88\83I,K,V. â\9dªG,Kâ\9d« â\8a¢ V ![h,a] & L = K.â\93\91[I]V.
 /2 width=3 by cnv_inv_zero_aux/ qed-.
 
 fact cnv_inv_lref_aux (h) (a):
-     â\88\80G,L,X. â¦\83G,Lâ¦\84 ⊢ X ![h,a] → ∀i. X = #(↑i) →
-     â\88\83â\88\83I,K. â¦\83G,Kâ¦\84 â\8a¢ #i ![h,a] & L = K.â\93\98{I}.
+     â\88\80G,L,X. â\9dªG,Lâ\9d« ⊢ X ![h,a] → ∀i. X = #(↑i) →
+     â\88\83â\88\83I,K. â\9dªG,Kâ\9d« â\8a¢ #i ![h,a] & L = K.â\93\98[I].
 #h #a #G #L #X * -G -L -X
 [ #G #L #s #j #H destruct
 | #I #G #K #V #_ #j #H destruct
@@ -69,11 +69,11 @@ fact cnv_inv_lref_aux (h) (a):
 qed-.
 
 lemma cnv_inv_lref (h) (a):
-      â\88\80G,L,i. â¦\83G,Lâ¦\84 ⊢ #↑i ![h,a] →
-      â\88\83â\88\83I,K. â¦\83G,Kâ¦\84 â\8a¢ #i ![h,a] & L = K.â\93\98{I}.
+      â\88\80G,L,i. â\9dªG,Lâ\9d« ⊢ #↑i ![h,a] →
+      â\88\83â\88\83I,K. â\9dªG,Kâ\9d« â\8a¢ #i ![h,a] & L = K.â\93\98[I].
 /2 width=3 by cnv_inv_lref_aux/ qed-.
 
-fact cnv_inv_gref_aux (h) (a): â\88\80G,L,X. â¦\83G,Lâ¦\84 ⊢ X ![h,a] → ∀l. X = §l → ⊥.
+fact cnv_inv_gref_aux (h) (a): â\88\80G,L,X. â\9dªG,Lâ\9d« ⊢ X ![h,a] → ∀l. X = §l → ⊥.
 #h #a #G #L #X * -G -L -X
 [ #G #L #s #l #H destruct
 | #I #G #K #V #_ #l #H destruct
@@ -85,13 +85,13 @@ fact cnv_inv_gref_aux (h) (a): ∀G,L,X. ⦃G,L⦄ ⊢ X ![h,a] → ∀l. X = §
 qed-.
 
 (* Basic_2A1: uses: snv_inv_gref *)
-lemma cnv_inv_gref (h) (a): â\88\80G,L,l. â¦\83G,Lâ¦\84 ⊢ §l ![h,a] → ⊥.
+lemma cnv_inv_gref (h) (a): â\88\80G,L,l. â\9dªG,Lâ\9d« ⊢ §l ![h,a] → ⊥.
 /2 width=8 by cnv_inv_gref_aux/ qed-.
 
 fact cnv_inv_bind_aux (h) (a):
-     â\88\80G,L,X. â¦\83G,Lâ¦\84 ⊢ X ![h,a] →
-     ∀p,I,V,T. X = ⓑ{p,I}V.T →
-     â\88§â\88§ â¦\83G,Lâ¦\84 â\8a¢ V ![h,a] & â¦\83G,L.â\93\91{I}Vâ¦\84 ⊢ T ![h,a].
+     â\88\80G,L,X. â\9dªG,Lâ\9d« ⊢ X ![h,a] →
+     ∀p,I,V,T. X = ⓑ[p,I]V.T →
+     â\88§â\88§ â\9dªG,Lâ\9d« â\8a¢ V ![h,a] & â\9dªG,L.â\93\91[I]Vâ\9d« ⊢ T ![h,a].
 #h #a #G #L #X * -G -L -X
 [ #G #L #s #q #Z #X1 #X2 #H destruct
 | #I #G #K #V #_ #q #Z #X1 #X2 #H destruct
@@ -104,14 +104,14 @@ qed-.
 
 (* Basic_2A1: uses: snv_inv_bind *)
 lemma cnv_inv_bind (h) (a):
-      â\88\80p,I,G,L,V,T. â¦\83G,Lâ¦\84 â\8a¢ â\93\91{p,I}V.T ![h,a] →
-      â\88§â\88§ â¦\83G,Lâ¦\84 â\8a¢ V ![h,a] & â¦\83G,L.â\93\91{I}Vâ¦\84 ⊢ T ![h,a].
+      â\88\80p,I,G,L,V,T. â\9dªG,Lâ\9d« â\8a¢ â\93\91[p,I]V.T ![h,a] →
+      â\88§â\88§ â\9dªG,Lâ\9d« â\8a¢ V ![h,a] & â\9dªG,L.â\93\91[I]Vâ\9d« ⊢ T ![h,a].
 /2 width=4 by cnv_inv_bind_aux/ qed-.
 
 fact cnv_inv_appl_aux (h) (a):
-     â\88\80G,L,X. â¦\83G,Lâ¦\84 ⊢ X ![h,a] → ∀V,T. X = ⓐV.T →
-     â\88\83â\88\83n,p,W0,U0. ad a n & â¦\83G,Lâ¦\84 â\8a¢ V ![h,a] & â¦\83G,Lâ¦\84 ⊢ T ![h,a] &
-                  â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡*[1,h] W0 & â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] â\93\9b{p}W0.U0.
+     â\88\80G,L,X. â\9dªG,Lâ\9d« ⊢ X ![h,a] → ∀V,T. X = ⓐV.T →
+     â\88\83â\88\83n,p,W0,U0. ad a n & â\9dªG,Lâ\9d« â\8a¢ V ![h,a] & â\9dªG,Lâ\9d« ⊢ T ![h,a] &
+                  â\9dªG,Lâ\9d« â\8a¢ V â\9e¡*[1,h] W0 & â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[n,h] â\93\9b[p]W0.U0.
 #h #a #G #L #X * -L -X
 [ #G #L #s #X1 #X2 #H destruct
 | #I #G #K #V #_ #X1 #X2 #H destruct
@@ -124,15 +124,15 @@ qed-.
 
 (* Basic_2A1: uses: snv_inv_appl *)
 lemma cnv_inv_appl (h) (a):
-      â\88\80G,L,V,T. â¦\83G,Lâ¦\84 ⊢ ⓐV.T ![h,a] →
-      â\88\83â\88\83n,p,W0,U0. ad a n & â¦\83G,Lâ¦\84 â\8a¢ V ![h,a] & â¦\83G,Lâ¦\84 ⊢ T ![h,a] &
-                   â¦\83G,Lâ¦\84 â\8a¢ V â\9e¡*[1,h] W0 & â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] â\93\9b{p}W0.U0.
+      â\88\80G,L,V,T. â\9dªG,Lâ\9d« ⊢ ⓐV.T ![h,a] →
+      â\88\83â\88\83n,p,W0,U0. ad a n & â\9dªG,Lâ\9d« â\8a¢ V ![h,a] & â\9dªG,Lâ\9d« ⊢ T ![h,a] &
+                   â\9dªG,Lâ\9d« â\8a¢ V â\9e¡*[1,h] W0 & â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[n,h] â\93\9b[p]W0.U0.
 /2 width=3 by cnv_inv_appl_aux/ qed-.
 
 fact cnv_inv_cast_aux (h) (a):
-     â\88\80G,L,X. â¦\83G,Lâ¦\84 ⊢ X ![h,a] → ∀U,T. X = ⓝU.T →
-     â\88\83â\88\83U0. â¦\83G,Lâ¦\84 â\8a¢ U ![h,a] & â¦\83G,Lâ¦\84 ⊢ T ![h,a] &
-           â¦\83G,Lâ¦\84 â\8a¢ U â\9e¡*[h] U0 & â¦\83G,Lâ¦\84 ⊢ T ➡*[1,h] U0.
+     â\88\80G,L,X. â\9dªG,Lâ\9d« ⊢ X ![h,a] → ∀U,T. X = ⓝU.T →
+     â\88\83â\88\83U0. â\9dªG,Lâ\9d« â\8a¢ U ![h,a] & â\9dªG,Lâ\9d« ⊢ T ![h,a] &
+           â\9dªG,Lâ\9d« â\8a¢ U â\9e¡*[h] U0 & â\9dªG,Lâ\9d« ⊢ T ➡*[1,h] U0.
 #h #a #G #L #X * -G -L -X
 [ #G #L #s #X1 #X2 #H destruct
 | #I #G #K #V #_ #X1 #X2 #H destruct
@@ -145,16 +145,16 @@ qed-.
 
 (* Basic_2A1: uses: snv_inv_cast *)
 lemma cnv_inv_cast (h) (a):
-      â\88\80G,L,U,T. â¦\83G,Lâ¦\84 ⊢ ⓝU.T ![h,a] →
-      â\88\83â\88\83U0. â¦\83G,Lâ¦\84 â\8a¢ U ![h,a] & â¦\83G,Lâ¦\84 ⊢ T ![h,a] &
-            â¦\83G,Lâ¦\84 â\8a¢ U â\9e¡*[h] U0 & â¦\83G,Lâ¦\84 ⊢ T ➡*[1,h] U0.
+      â\88\80G,L,U,T. â\9dªG,Lâ\9d« ⊢ ⓝU.T ![h,a] →
+      â\88\83â\88\83U0. â\9dªG,Lâ\9d« â\8a¢ U ![h,a] & â\9dªG,Lâ\9d« ⊢ T ![h,a] &
+            â\9dªG,Lâ\9d« â\8a¢ U â\9e¡*[h] U0 & â\9dªG,Lâ\9d« ⊢ T ➡*[1,h] U0.
 /2 width=3 by cnv_inv_cast_aux/ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
 lemma cnv_fwd_flat (h) (a) (I) (G) (L):
-      â\88\80V,T. â¦\83G,Lâ¦\84 â\8a¢ â\93\95{I}V.T ![h,a] →
-      â\88§â\88§ â¦\83G,Lâ¦\84 â\8a¢ V ![h,a] & â¦\83G,Lâ¦\84 ⊢ T ![h,a].
+      â\88\80V,T. â\9dªG,Lâ\9d« â\8a¢ â\93\95[I]V.T ![h,a] →
+      â\88§â\88§ â\9dªG,Lâ\9d« â\8a¢ V ![h,a] & â\9dªG,Lâ\9d« ⊢ T ![h,a].
 #h #a * #G #L #V #T #H
 [ elim (cnv_inv_appl … H) #n #p #W #U #_ #HV #HT #_ #_
 | elim (cnv_inv_cast … H) #U #HV #HT #_ #_
@@ -162,7 +162,7 @@ lemma cnv_fwd_flat (h) (a) (I) (G) (L):
 qed-.
 
 lemma cnv_fwd_pair_sn (h) (a) (I) (G) (L):
-      â\88\80V,T. â¦\83G,Lâ¦\84 â\8a¢ â\91¡{I}V.T ![h,a] â\86\92 â¦\83G,Lâ¦\84 ⊢ V ![h,a].
+      â\88\80V,T. â\9dªG,Lâ\9d« â\8a¢ â\91¡[I]V.T ![h,a] â\86\92 â\9dªG,Lâ\9d« ⊢ V ![h,a].
 #h #a * [ #p ] #I #G #L #V #T #H
 [ elim (cnv_inv_bind … H) -H #HV #_
 | elim (cnv_fwd_flat … H) -H #HV #_