X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fstatic%2Faaa.ma;h=a13ca0f16269fbc07b0f8ba7f6d229be43595d59;hp=04f70ba916556703faec40858e62729f7f1010d9;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hpb=3b7b8afcb429a60d716d5226a5b6ab0d003228b1

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/aaa.ma b/matita/matita/contribs/lambdadelta/static_2/static/aaa.ma
index 04f70ba91..a13ca0f16 100644
--- a/matita/matita/contribs/lambdadelta/static_2/static/aaa.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/aaa.ma
@@ -24,12 +24,12 @@ include "static_2/syntax/genv.ma".
 (* activate genv *)
 inductive aaa: relation4 genv lenv term aarity ≝
 | aaa_sort: ∀G,L,s. aaa G L (⋆s) (⓪)
-| aaa_zero: ∀I,G,L,V,B. aaa G L V B → aaa G (L.ⓑ{I}V) (#0) B
-| aaa_lref: ∀I,G,L,A,i. aaa G L (#i) A → aaa G (L.ⓘ{I}) (#↑i) A
+| aaa_zero: ∀I,G,L,V,B. aaa G L V B → aaa G (L.ⓑ[I]V) (#0) B
+| aaa_lref: ∀I,G,L,A,i. aaa G L (#i) A → aaa G (L.ⓘ[I]) (#↑i) A
 | aaa_abbr: ∀p,G,L,V,T,B,A.
-            aaa G L V B → aaa G (L.ⓓV) T A → aaa G L (ⓓ{p}V.T) A
+            aaa G L V B → aaa G (L.ⓓV) T A → aaa G L (ⓓ[p]V.T) A
 | aaa_abst: ∀p,G,L,V,T,B,A.
-            aaa G L V B → aaa G (L.ⓛV) T A → aaa G L (ⓛ{p}V.T) (②B.A)
+            aaa G L V B → aaa G (L.ⓛV) T A → aaa G L (ⓛ[p]V.T) (②B.A)
 | aaa_appl: ∀G,L,V,T,B,A. aaa G L V B → aaa G L T (②B.A) → aaa G L (ⓐV.T) A
 | aaa_cast: ∀G,L,V,T,A. aaa G L V A → aaa G L T A → aaa G L (ⓝV.T) A
 .
@@ -39,7 +39,7 @@ interpretation "atomic arity assignment (term)"
 
 (* Basic inversion lemmas ***************************************************)
 
-fact aaa_inv_sort_aux: ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → ∀s. T = ⋆s → A = ⓪.
+fact aaa_inv_sort_aux: ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → ∀s. T = ⋆s → A = ⓪.
 #G #L #T #A * -G -L -T -A //
 [ #I #G #L #V #B #_ #s #H destruct
 | #I #G #L #A #i #_ #s #H destruct
@@ -50,11 +50,11 @@ fact aaa_inv_sort_aux: ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → ∀s. T = ⋆s →
 ]
 qed-.
 
-lemma aaa_inv_sort: ∀G,L,A,s. ⦃G,L⦄ ⊢ ⋆s ⁝ A → A = ⓪.
+lemma aaa_inv_sort: ∀G,L,A,s. ❪G,L❫ ⊢ ⋆s ⁝ A → A = ⓪.
 /2 width=6 by aaa_inv_sort_aux/ qed-.
 
-fact aaa_inv_zero_aux: ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → T = #0 →
-                       ∃∃I,K,V. L = K.ⓑ{I}V & ⦃G,K⦄ ⊢ V ⁝ A.
+fact aaa_inv_zero_aux: ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → T = #0 →
+                       ∃∃I,K,V. L = K.ⓑ[I]V & ❪G,K❫ ⊢ V ⁝ A.
 #G #L #T #A * -G -L -T -A /2 width=5 by ex2_3_intro/
 [ #G #L #s #H destruct
 | #I #G #L #A #i #_ #H destruct
@@ -65,12 +65,12 @@ fact aaa_inv_zero_aux: ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → T = #0 →
 ]
 qed-.
 
-lemma aaa_inv_zero: ∀G,L,A. ⦃G,L⦄ ⊢ #0 ⁝ A →
-                    ∃∃I,K,V. L = K.ⓑ{I}V & ⦃G,K⦄ ⊢ V ⁝ A.
+lemma aaa_inv_zero: ∀G,L,A. ❪G,L❫ ⊢ #0 ⁝ A →
+                    ∃∃I,K,V. L = K.ⓑ[I]V & ❪G,K❫ ⊢ V ⁝ A.
 /2 width=3 by aaa_inv_zero_aux/ qed-.
 
-fact aaa_inv_lref_aux: ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → ∀i. T = #(↑i) →
-                       ∃∃I,K. L = K.ⓘ{I} & ⦃G,K⦄ ⊢ #i ⁝ A.
+fact aaa_inv_lref_aux: ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → ∀i. T = #(↑i) →
+                       ∃∃I,K. L = K.ⓘ[I] & ❪G,K❫ ⊢ #i ⁝ A.
 #G #L #T #A * -G -L -T -A
 [ #G #L #s #j #H destruct
 | #I #G #L #V #B #_ #j #H destruct
@@ -82,11 +82,11 @@ fact aaa_inv_lref_aux: ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → ∀i. T = #(↑i) 
 ]
 qed-.
 
-lemma aaa_inv_lref: ∀G,L,A,i. ⦃G,L⦄ ⊢ #↑i ⁝ A →
-                    ∃∃I,K. L = K.ⓘ{I} & ⦃G,K⦄ ⊢ #i ⁝ A.
+lemma aaa_inv_lref: ∀G,L,A,i. ❪G,L❫ ⊢ #↑i ⁝ A →
+                    ∃∃I,K. L = K.ⓘ[I] & ❪G,K❫ ⊢ #i ⁝ A.
 /2 width=3 by aaa_inv_lref_aux/ qed-.
 
-fact aaa_inv_gref_aux: ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → ∀l. T = §l → ⊥.
+fact aaa_inv_gref_aux: ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → ∀l. T = §l → ⊥.
 #G #L #T #A * -G -L -T -A
 [ #G #L #s #k #H destruct
 | #I #G #L #V #B #_ #k #H destruct
@@ -98,11 +98,11 @@ fact aaa_inv_gref_aux: ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → ∀l. T = §l → 
 ]
 qed-.
 
-lemma aaa_inv_gref: ∀G,L,A,l. ⦃G,L⦄ ⊢ §l ⁝ A → ⊥.
+lemma aaa_inv_gref: ∀G,L,A,l. ❪G,L❫ ⊢ §l ⁝ A → ⊥.
 /2 width=7 by aaa_inv_gref_aux/ qed-.
 
-fact aaa_inv_abbr_aux: ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → ∀p,W,U. T = ⓓ{p}W.U →
-                       ∃∃B. ⦃G,L⦄ ⊢ W ⁝ B & ⦃G,L.ⓓW⦄ ⊢ U ⁝ A.
+fact aaa_inv_abbr_aux: ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → ∀p,W,U. T = ⓓ[p]W.U →
+                       ∃∃B. ❪G,L❫ ⊢ W ⁝ B & ❪G,L.ⓓW❫ ⊢ U ⁝ A.
 #G #L #T #A * -G -L -T -A
 [ #G #L #s #q #W #U #H destruct
 | #I #G #L #V #B #_ #q #W #U #H destruct
@@ -114,12 +114,12 @@ fact aaa_inv_abbr_aux: ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → ∀p,W,U. T = ⓓ{p
 ]
 qed-.
 
-lemma aaa_inv_abbr: ∀p,G,L,V,T,A. ⦃G,L⦄ ⊢ ⓓ{p}V.T ⁝ A →
-                    ∃∃B. ⦃G,L⦄ ⊢ V ⁝ B & ⦃G,L.ⓓV⦄ ⊢ T ⁝ A.
+lemma aaa_inv_abbr: ∀p,G,L,V,T,A. ❪G,L❫ ⊢ ⓓ[p]V.T ⁝ A →
+                    ∃∃B. ❪G,L❫ ⊢ V ⁝ B & ❪G,L.ⓓV❫ ⊢ T ⁝ A.
 /2 width=4 by aaa_inv_abbr_aux/ qed-.
 
-fact aaa_inv_abst_aux: ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → ∀p,W,U. T = ⓛ{p}W.U →
-                       ∃∃B1,B2. ⦃G,L⦄ ⊢ W ⁝ B1 & ⦃G,L.ⓛW⦄ ⊢ U ⁝ B2 & A = ②B1.B2.
+fact aaa_inv_abst_aux: ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → ∀p,W,U. T = ⓛ[p]W.U →
+                       ∃∃B1,B2. ❪G,L❫ ⊢ W ⁝ B1 & ❪G,L.ⓛW❫ ⊢ U ⁝ B2 & A = ②B1.B2.
 #G #L #T #A * -G -L -T -A
 [ #G #L #s #q #W #U #H destruct
 | #I #G #L #V #B #_ #q #W #U #H destruct
@@ -131,12 +131,12 @@ fact aaa_inv_abst_aux: ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → ∀p,W,U. T = ⓛ{p
 ]
 qed-.
 
-lemma aaa_inv_abst: ∀p,G,L,W,T,A. ⦃G,L⦄ ⊢ ⓛ{p}W.T ⁝ A →
-                    ∃∃B1,B2. ⦃G,L⦄ ⊢ W ⁝ B1 & ⦃G,L.ⓛW⦄ ⊢ T ⁝ B2 & A = ②B1.B2.
+lemma aaa_inv_abst: ∀p,G,L,W,T,A. ❪G,L❫ ⊢ ⓛ[p]W.T ⁝ A →
+                    ∃∃B1,B2. ❪G,L❫ ⊢ W ⁝ B1 & ❪G,L.ⓛW❫ ⊢ T ⁝ B2 & A = ②B1.B2.
 /2 width=4 by aaa_inv_abst_aux/ qed-.
 
-fact aaa_inv_appl_aux: ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → ∀W,U. T = ⓐW.U →
-                       ∃∃B. ⦃G,L⦄ ⊢ W ⁝ B & ⦃G,L⦄ ⊢ U ⁝ ②B.A.
+fact aaa_inv_appl_aux: ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → ∀W,U. T = ⓐW.U →
+                       ∃∃B. ❪G,L❫ ⊢ W ⁝ B & ❪G,L❫ ⊢ U ⁝ ②B.A.
 #G #L #T #A * -G -L -T -A
 [ #G #L #s #W #U #H destruct
 | #I #G #L #V #B #_ #W #U #H destruct
@@ -148,12 +148,12 @@ fact aaa_inv_appl_aux: ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → ∀W,U. T = ⓐW.U
 ]
 qed-.
 
-lemma aaa_inv_appl: ∀G,L,V,T,A. ⦃G,L⦄ ⊢ ⓐV.T ⁝ A →
-                    ∃∃B. ⦃G,L⦄ ⊢ V ⁝ B & ⦃G,L⦄ ⊢ T ⁝ ②B.A.
+lemma aaa_inv_appl: ∀G,L,V,T,A. ❪G,L❫ ⊢ ⓐV.T ⁝ A →
+                    ∃∃B. ❪G,L❫ ⊢ V ⁝ B & ❪G,L❫ ⊢ T ⁝ ②B.A.
 /2 width=3 by aaa_inv_appl_aux/ qed-.
 
-fact aaa_inv_cast_aux: ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → ∀W,U. T = ⓝW.U →
-                       ⦃G,L⦄ ⊢ W ⁝ A ∧ ⦃G,L⦄ ⊢ U ⁝ A.
+fact aaa_inv_cast_aux: ∀G,L,T,A. ❪G,L❫ ⊢ T ⁝ A → ∀W,U. T = ⓝW.U →
+                       ❪G,L❫ ⊢ W ⁝ A ∧ ❪G,L❫ ⊢ U ⁝ A.
 #G #L #T #A * -G -L -T -A
 [ #G #L #s #W #U #H destruct
 | #I #G #L #V #B #_ #W #U #H destruct
@@ -165,6 +165,6 @@ fact aaa_inv_cast_aux: ∀G,L,T,A. ⦃G,L⦄ ⊢ T ⁝ A → ∀W,U. T = ⓝW.U
 ]
 qed-.
 
-lemma aaa_inv_cast: ∀G,L,W,T,A. ⦃G,L⦄ ⊢ ⓝW.T ⁝ A →
-                    ⦃G,L⦄ ⊢ W ⁝ A ∧ ⦃G,L⦄ ⊢ T ⁝ A.
+lemma aaa_inv_cast: ∀G,L,W,T,A. ❪G,L❫ ⊢ ⓝW.T ⁝ A →
+                    ❪G,L❫ ⊢ W ⁝ A ∧ ❪G,L❫ ⊢ T ⁝ A.
 /2 width=3 by aaa_inv_cast_aux/ qed-.