update in ground static_2 basic_2 apps_2

[helm.git] / matita / matita / contribs / lambdadelta / static_2 / static / aaa.ma

diff --git a/matita/matita/contribs/lambdadelta/static_2/static/aaa.ma b/matita/matita/contribs/lambdadelta/static_2/static/aaa.ma
index 841c85be25ee7d28cdb5d43d95583518c72ed49d..bb18f69f480abbbc5a91f652d79f56697e0eedaf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/static_2/static/aaa.ma
+++ b/matita/matita/contribs/lambdadelta/static_2/static/aaa.ma
@@ -39,7 +39,7 @@ interpretation "atomic arity assignment (term)"
 
 (* Basic inversion lemmas ***************************************************)
 
-fact aaa_inv_sort_aux: â\88\80G,L,T,A. â\9dªG,Lâ\9d« ⊢ T ⁝ A → ∀s. T = ⋆s → A = ⓪.
+fact aaa_inv_sort_aux: â\88\80G,L,T,A. â\9d¨G,Lâ\9d© ⊢ 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: â\88\80G,L,A,s. â\9dªG,Lâ\9d« ⊢ ⋆s ⁝ A → A = ⓪.
+lemma aaa_inv_sort: â\88\80G,L,A,s. â\9d¨G,Lâ\9d© ⊢ ⋆s ⁝ A → A = ⓪.
 /2 width=6 by aaa_inv_sort_aux/ qed-.
 
-fact aaa_inv_zero_aux: â\88\80G,L,T,A. â\9dªG,Lâ\9d« ⊢ T ⁝ A → T = #0 →
-                       â\88\83â\88\83I,K,V. L = K.â\93\91[I]V & â\9dªG,Kâ\9d« ⊢ V ⁝ A.
+fact aaa_inv_zero_aux: â\88\80G,L,T,A. â\9d¨G,Lâ\9d© ⊢ T ⁝ A → T = #0 →
+                       â\88\83â\88\83I,K,V. L = K.â\93\91[I]V & â\9d¨G,Kâ\9d© ⊢ 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: â\88\80G,L,A. â\9dªG,Lâ\9d« ⊢ #0 ⁝ A →
-                    â\88\83â\88\83I,K,V. L = K.â\93\91[I]V & â\9dªG,Kâ\9d« ⊢ V ⁝ A.
+lemma aaa_inv_zero: â\88\80G,L,A. â\9d¨G,Lâ\9d© ⊢ #0 ⁝ A →
+                    â\88\83â\88\83I,K,V. L = K.â\93\91[I]V & â\9d¨G,Kâ\9d© ⊢ V ⁝ A.
 /2 width=3 by aaa_inv_zero_aux/ qed-.
 
-fact aaa_inv_lref_aux: â\88\80G,L,T,A. â\9dªG,Lâ\9d« ⊢ T ⁝ A → ∀i. T = #(↑i) →
-                       â\88\83â\88\83I,K. L = K.â\93\98[I] & â\9dªG,Kâ\9d« ⊢ #i ⁝ A.
+fact aaa_inv_lref_aux: â\88\80G,L,T,A. â\9d¨G,Lâ\9d© ⊢ T ⁝ A → ∀i. T = #(↑i) →
+                       â\88\83â\88\83I,K. L = K.â\93\98[I] & â\9d¨G,Kâ\9d© ⊢ #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: â\88\80G,L,A,i. â\9dªG,Lâ\9d« ⊢ #↑i ⁝ A →
-                    â\88\83â\88\83I,K. L = K.â\93\98[I] & â\9dªG,Kâ\9d« ⊢ #i ⁝ A.
+lemma aaa_inv_lref: â\88\80G,L,A,i. â\9d¨G,Lâ\9d© ⊢ #↑i ⁝ A →
+                    â\88\83â\88\83I,K. L = K.â\93\98[I] & â\9d¨G,Kâ\9d© ⊢ #i ⁝ A.
 /2 width=3 by aaa_inv_lref_aux/ qed-.
 
-fact aaa_inv_gref_aux: â\88\80G,L,T,A. â\9dªG,Lâ\9d« ⊢ T ⁝ A → ∀l. T = §l → ⊥.
+fact aaa_inv_gref_aux: â\88\80G,L,T,A. â\9d¨G,Lâ\9d© ⊢ 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: â\88\80G,L,A,l. â\9dªG,Lâ\9d« ⊢ §l ⁝ A → ⊥.
+lemma aaa_inv_gref: â\88\80G,L,A,l. â\9d¨G,Lâ\9d© ⊢ §l ⁝ A → ⊥.
 /2 width=7 by aaa_inv_gref_aux/ qed-.
 
-fact aaa_inv_abbr_aux: â\88\80G,L,T,A. â\9dªG,Lâ\9d« ⊢ T ⁝ A → ∀p,W,U. T = ⓓ[p]W.U →
-                       â\88\83â\88\83B. â\9dªG,Lâ\9d« â\8a¢ W â\81\9d B & â\9dªG,L.â\93\93Wâ\9d« ⊢ U ⁝ A.
+fact aaa_inv_abbr_aux: â\88\80G,L,T,A. â\9d¨G,Lâ\9d© ⊢ T ⁝ A → ∀p,W,U. T = ⓓ[p]W.U →
+                       â\88\83â\88\83B. â\9d¨G,Lâ\9d© â\8a¢ W â\81\9d B & â\9d¨G,L.â\93\93Wâ\9d© ⊢ 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: â\88\80p,G,L,V,T,A. â\9dªG,Lâ\9d« ⊢ ⓓ[p]V.T ⁝ A →
-                    â\88\83â\88\83B. â\9dªG,Lâ\9d« â\8a¢ V â\81\9d B & â\9dªG,L.â\93\93Vâ\9d« ⊢ T ⁝ A.
+lemma aaa_inv_abbr: â\88\80p,G,L,V,T,A. â\9d¨G,Lâ\9d© ⊢ ⓓ[p]V.T ⁝ A →
+                    â\88\83â\88\83B. â\9d¨G,Lâ\9d© â\8a¢ V â\81\9d B & â\9d¨G,L.â\93\93Vâ\9d© ⊢ T ⁝ A.
 /2 width=4 by aaa_inv_abbr_aux/ qed-.
 
-fact aaa_inv_abst_aux: â\88\80G,L,T,A. â\9dªG,Lâ\9d« ⊢ T ⁝ A → ∀p,W,U. T = ⓛ[p]W.U →
-                       â\88\83â\88\83B1,B2. â\9dªG,Lâ\9d« â\8a¢ W â\81\9d B1 & â\9dªG,L.â\93\9bWâ\9d« ⊢ U ⁝ B2 & A = ②B1.B2.
+fact aaa_inv_abst_aux: â\88\80G,L,T,A. â\9d¨G,Lâ\9d© ⊢ T ⁝ A → ∀p,W,U. T = ⓛ[p]W.U →
+                       â\88\83â\88\83B1,B2. â\9d¨G,Lâ\9d© â\8a¢ W â\81\9d B1 & â\9d¨G,L.â\93\9bWâ\9d© ⊢ 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: â\88\80p,G,L,W,T,A. â\9dªG,Lâ\9d« ⊢ ⓛ[p]W.T ⁝ A →
-                    â\88\83â\88\83B1,B2. â\9dªG,Lâ\9d« â\8a¢ W â\81\9d B1 & â\9dªG,L.â\93\9bWâ\9d« ⊢ T ⁝ B2 & A = ②B1.B2.
+lemma aaa_inv_abst: â\88\80p,G,L,W,T,A. â\9d¨G,Lâ\9d© ⊢ ⓛ[p]W.T ⁝ A →
+                    â\88\83â\88\83B1,B2. â\9d¨G,Lâ\9d© â\8a¢ W â\81\9d B1 & â\9d¨G,L.â\93\9bWâ\9d© ⊢ T ⁝ B2 & A = ②B1.B2.
 /2 width=4 by aaa_inv_abst_aux/ qed-.
 
-fact aaa_inv_appl_aux: â\88\80G,L,T,A. â\9dªG,Lâ\9d« ⊢ T ⁝ A → ∀W,U. T = ⓐW.U →
-                       â\88\83â\88\83B. â\9dªG,Lâ\9d« â\8a¢ W â\81\9d B & â\9dªG,Lâ\9d« ⊢ U ⁝ ②B.A.
+fact aaa_inv_appl_aux: â\88\80G,L,T,A. â\9d¨G,Lâ\9d© ⊢ T ⁝ A → ∀W,U. T = ⓐW.U →
+                       â\88\83â\88\83B. â\9d¨G,Lâ\9d© â\8a¢ W â\81\9d B & â\9d¨G,Lâ\9d© ⊢ 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: â\88\80G,L,V,T,A. â\9dªG,Lâ\9d« ⊢ ⓐV.T ⁝ A →
-                    â\88\83â\88\83B. â\9dªG,Lâ\9d« â\8a¢ V â\81\9d B & â\9dªG,Lâ\9d« ⊢ T ⁝ ②B.A.
+lemma aaa_inv_appl: â\88\80G,L,V,T,A. â\9d¨G,Lâ\9d© ⊢ ⓐV.T ⁝ A →
+                    â\88\83â\88\83B. â\9d¨G,Lâ\9d© â\8a¢ V â\81\9d B & â\9d¨G,Lâ\9d© ⊢ T ⁝ ②B.A.
 /2 width=3 by aaa_inv_appl_aux/ qed-.
 
-fact aaa_inv_cast_aux: â\88\80G,L,T,A. â\9dªG,Lâ\9d« ⊢ T ⁝ A → ∀W,U. T = ⓝW.U →
-                       â\9dªG,Lâ\9d« â\8a¢ W â\81\9d A â\88§ â\9dªG,Lâ\9d« ⊢ U ⁝ A.
+fact aaa_inv_cast_aux: â\88\80G,L,T,A. â\9d¨G,Lâ\9d© ⊢ T ⁝ A → ∀W,U. T = ⓝW.U →
+                       â\9d¨G,Lâ\9d© â\8a¢ W â\81\9d A â\88§ â\9d¨G,Lâ\9d© ⊢ 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: â\88\80G,L,W,T,A. â\9dªG,Lâ\9d« ⊢ ⓝW.T ⁝ A →
-                    â\9dªG,Lâ\9d« â\8a¢ W â\81\9d A â\88§ â\9dªG,Lâ\9d« ⊢ T ⁝ A.
+lemma aaa_inv_cast: â\88\80G,L,W,T,A. â\9d¨G,Lâ\9d© ⊢ ⓝW.T ⁝ A →
+                    â\9d¨G,Lâ\9d© â\8a¢ W â\81\9d A â\88§ â\9d¨G,Lâ\9d© ⊢ T ⁝ A.
 /2 width=3 by aaa_inv_cast_aux/ qed-.