X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv.ma;h=256b798b50a2c1694874654586e618844e95aa22;hp=14da27905e1dadb6a30b6719580c579550a28f73;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hpb=3b7b8afcb429a60d716d5226a5b6ab0d003228b1

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
index 14da27905..256b798b5 100644
--- 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 →
-            ⦃G,L⦄ ⊢ V ➡*[1,h] W0 → ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W0.U0 → cnv h a G L (ⓐV.T)
+            ❪G,L❫ ⊢ V ➡*[1,h] W0 → ❪G,L❫ ⊢ T ➡*[n,h] ⓛ[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 →
-            ⦃G,L⦄ ⊢ U ➡*[h] U0 → ⦃G,L⦄ ⊢ T ➡*[1,h] U0 → cnv h a G L (ⓝU.T)
+            ❪G,L❫ ⊢ U ➡*[h] U0 → ❪G,L❫ ⊢ 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):
-     ∀G,L,X. ⦃G,L⦄ ⊢ X ![h,a] → X = #0 →
-     ∃∃I,K,V. ⦃G,K⦄ ⊢ V ![h,a] & L = K.ⓑ{I}V.
+     ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] → X = #0 →
+     ∃∃I,K,V. ❪G,K❫ ⊢ V ![h,a] & L = K.ⓑ[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):
-      ∀G,L. ⦃G,L⦄ ⊢ #0 ![h,a] →
-      ∃∃I,K,V. ⦃G,K⦄ ⊢ V ![h,a] & L = K.ⓑ{I}V.
+      ∀G,L. ❪G,L❫ ⊢ #0 ![h,a] →
+      ∃∃I,K,V. ❪G,K❫ ⊢ V ![h,a] & L = K.ⓑ[I]V.
 /2 width=3 by cnv_inv_zero_aux/ qed-.
 
 fact cnv_inv_lref_aux (h) (a):
-     ∀G,L,X. ⦃G,L⦄ ⊢ X ![h,a] → ∀i. X = #(↑i) →
-     ∃∃I,K. ⦃G,K⦄ ⊢ #i ![h,a] & L = K.ⓘ{I}.
+     ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] → ∀i. X = #(↑i) →
+     ∃∃I,K. ❪G,K❫ ⊢ #i ![h,a] & L = K.ⓘ[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):
-      ∀G,L,i. ⦃G,L⦄ ⊢ #↑i ![h,a] →
-      ∃∃I,K. ⦃G,K⦄ ⊢ #i ![h,a] & L = K.ⓘ{I}.
+      ∀G,L,i. ❪G,L❫ ⊢ #↑i ![h,a] →
+      ∃∃I,K. ❪G,K❫ ⊢ #i ![h,a] & L = K.ⓘ[I].
 /2 width=3 by cnv_inv_lref_aux/ qed-.
 
-fact cnv_inv_gref_aux (h) (a): ∀G,L,X. ⦃G,L⦄ ⊢ X ![h,a] → ∀l. X = §l → ⊥.
+fact cnv_inv_gref_aux (h) (a): ∀G,L,X. ❪G,L❫ ⊢ 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): ∀G,L,l. ⦃G,L⦄ ⊢ §l ![h,a] → ⊥.
+lemma cnv_inv_gref (h) (a): ∀G,L,l. ❪G,L❫ ⊢ §l ![h,a] → ⊥.
 /2 width=8 by cnv_inv_gref_aux/ qed-.
 
 fact cnv_inv_bind_aux (h) (a):
-     ∀G,L,X. ⦃G,L⦄ ⊢ X ![h,a] →
-     ∀p,I,V,T. X = ⓑ{p,I}V.T →
-     ∧∧ ⦃G,L⦄ ⊢ V ![h,a] & ⦃G,L.ⓑ{I}V⦄ ⊢ T ![h,a].
+     ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] →
+     ∀p,I,V,T. X = ⓑ[p,I]V.T →
+     ∧∧ ❪G,L❫ ⊢ V ![h,a] & ❪G,L.ⓑ[I]V❫ ⊢ 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):
-      ∀p,I,G,L,V,T. ⦃G,L⦄ ⊢ ⓑ{p,I}V.T ![h,a] →
-      ∧∧ ⦃G,L⦄ ⊢ V ![h,a] & ⦃G,L.ⓑ{I}V⦄ ⊢ T ![h,a].
+      ∀p,I,G,L,V,T. ❪G,L❫ ⊢ ⓑ[p,I]V.T ![h,a] →
+      ∧∧ ❪G,L❫ ⊢ V ![h,a] & ❪G,L.ⓑ[I]V❫ ⊢ T ![h,a].
 /2 width=4 by cnv_inv_bind_aux/ qed-.
 
 fact cnv_inv_appl_aux (h) (a):
-     ∀G,L,X. ⦃G,L⦄ ⊢ X ![h,a] → ∀V,T. X = ⓐV.T →
-     ∃∃n,p,W0,U0. ad a n & ⦃G,L⦄ ⊢ V ![h,a] & ⦃G,L⦄ ⊢ T ![h,a] &
-                  ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W0.U0.
+     ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] → ∀V,T. X = ⓐV.T →
+     ∃∃n,p,W0,U0. ad a n & ❪G,L❫ ⊢ V ![h,a] & ❪G,L❫ ⊢ T ![h,a] &
+                  ❪G,L❫ ⊢ V ➡*[1,h] W0 & ❪G,L❫ ⊢ T ➡*[n,h] ⓛ[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):
-      ∀G,L,V,T. ⦃G,L⦄ ⊢ ⓐV.T ![h,a] →
-      ∃∃n,p,W0,U0. ad a n & ⦃G,L⦄ ⊢ V ![h,a] & ⦃G,L⦄ ⊢ T ![h,a] &
-                   ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[n,h] ⓛ{p}W0.U0.
+      ∀G,L,V,T. ❪G,L❫ ⊢ ⓐV.T ![h,a] →
+      ∃∃n,p,W0,U0. ad a n & ❪G,L❫ ⊢ V ![h,a] & ❪G,L❫ ⊢ T ![h,a] &
+                   ❪G,L❫ ⊢ V ➡*[1,h] W0 & ❪G,L❫ ⊢ T ➡*[n,h] ⓛ[p]W0.U0.
 /2 width=3 by cnv_inv_appl_aux/ qed-.
 
 fact cnv_inv_cast_aux (h) (a):
-     ∀G,L,X. ⦃G,L⦄ ⊢ X ![h,a] → ∀U,T. X = ⓝU.T →
-     ∃∃U0. ⦃G,L⦄ ⊢ U ![h,a] & ⦃G,L⦄ ⊢ T ![h,a] &
-           ⦃G,L⦄ ⊢ U ➡*[h] U0 & ⦃G,L⦄ ⊢ T ➡*[1,h] U0.
+     ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] → ∀U,T. X = ⓝU.T →
+     ∃∃U0. ❪G,L❫ ⊢ U ![h,a] & ❪G,L❫ ⊢ T ![h,a] &
+           ❪G,L❫ ⊢ U ➡*[h] U0 & ❪G,L❫ ⊢ 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):
-      ∀G,L,U,T. ⦃G,L⦄ ⊢ ⓝU.T ![h,a] →
-      ∃∃U0. ⦃G,L⦄ ⊢ U ![h,a] & ⦃G,L⦄ ⊢ T ![h,a] &
-            ⦃G,L⦄ ⊢ U ➡*[h] U0 & ⦃G,L⦄ ⊢ T ➡*[1,h] U0.
+      ∀G,L,U,T. ❪G,L❫ ⊢ ⓝU.T ![h,a] →
+      ∃∃U0. ❪G,L❫ ⊢ U ![h,a] & ❪G,L❫ ⊢ T ![h,a] &
+            ❪G,L❫ ⊢ U ➡*[h] U0 & ❪G,L❫ ⊢ 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):
-      ∀V,T. ⦃G,L⦄ ⊢ ⓕ{I}V.T ![h,a] →
-      ∧∧ ⦃G,L⦄ ⊢ V ![h,a] & ⦃G,L⦄ ⊢ T ![h,a].
+      ∀V,T. ❪G,L❫ ⊢ ⓕ[I]V.T ![h,a] →
+      ∧∧ ❪G,L❫ ⊢ V ![h,a] & ❪G,L❫ ⊢ 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):
-      ∀V,T. ⦃G,L⦄ ⊢ ②{I}V.T ![h,a] → ⦃G,L⦄ ⊢ V ![h,a].
+      ∀V,T. ❪G,L❫ ⊢ ②[I]V.T ![h,a] → ❪G,L❫ ⊢ 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 #_