(**************************************************************************)
include "basic_2/notation/relations/atomicarity_4.ma".
(**************************************************************************)
include "basic_2/notation/relations/atomicarity_4.ma".
-include "basic_2/grammar/aarity.ma".
-include "basic_2/grammar/lenv.ma".
-include "basic_2/grammar/genv.ma".
+include "basic_2/syntax/aarity.ma".
+include "basic_2/syntax/lenv.ma".
+include "basic_2/syntax/genv.ma".
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
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,V,A,i. aaa G L (#i) A → aaa G (L.ⓑ{I}V) (#⫯i) A
+| 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_abst: ∀p,G,L,V,T,B,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_abst: ∀p,G,L,V,T,B,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
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
| #p #G #L #V #T #B #A #_ #_ #s #H destruct
| #p #G #L #V #T #B #A #_ #_ #s #H destruct
| #G #L #V #T #B #A #_ #_ #s #H destruct
| #p #G #L #V #T #B #A #_ #_ #s #H destruct
| #p #G #L #V #T #B #A #_ #_ #s #H destruct
| #G #L #V #T #B #A #_ #_ #s #H destruct
∃∃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,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
| #p #G #L #V #T #B #A #_ #_ #H destruct
| #p #G #L #V #T #B #A #_ #_ #H destruct
| #G #L #V #T #B #A #_ #_ #H destruct
| #p #G #L #V #T #B #A #_ #_ #H destruct
| #p #G #L #V #T #B #A #_ #_ #H destruct
| #G #L #V #T #B #A #_ #_ #H destruct
∃∃I,K,V. L = K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ⁝ A.
/2 width=3 by aaa_inv_zero_aux/ qed-.
∃∃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: â\88\80G,L,T,A. â¦\83G, Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 â\88\80i. T = #(⫯i) →
- ∃∃I,K,V. L = K.ⓑ{I}V & ⦃G, K⦄ ⊢ #i ⁝ A.
+fact aaa_inv_lref_aux: â\88\80G,L,T,A. â¦\83G, Lâ¦\84 â\8a¢ T â\81\9d A â\86\92 â\88\80i. T = #(â\86\91i) →
+ ∃∃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
#G #L #T #A * -G -L -T -A
[ #G #L #s #j #H destruct
| #I #G #L #V #B #_ #j #H destruct
| #p #G #L #V #T #B #A #_ #_ #j #H destruct
| #p #G #L #V #T #B #A #_ #_ #j #H destruct
| #G #L #V #T #B #A #_ #_ #j #H destruct
| #p #G #L #V #T #B #A #_ #_ #j #H destruct
| #p #G #L #V #T #B #A #_ #_ #j #H destruct
| #G #L #V #T #B #A #_ #_ #j #H destruct
-lemma aaa_inv_lref: â\88\80G,L,A,i. â¦\83G, Lâ¦\84 â\8a¢ #⫯i ⁝ A →
- ∃∃I,K,V. L = K.ⓑ{I}V & ⦃G, K⦄ ⊢ #i ⁝ A.
+lemma aaa_inv_lref: â\88\80G,L,A,i. â¦\83G, Lâ¦\84 â\8a¢ #â\86\91i ⁝ 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 → ⊥.
#G #L #T #A * -G -L -T -A
[ #G #L #s #k #H destruct
| #I #G #L #V #B #_ #k #H destruct
/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 → ⊥.
#G #L #T #A * -G -L -T -A
[ #G #L #s #k #H destruct
| #I #G #L #V #B #_ #k #H destruct
| #p #G #L #V #T #B #A #_ #_ #k #H destruct
| #p #G #L #V #T #B #A #_ #_ #k #H destruct
| #G #L #V #T #B #A #_ #_ #k #H destruct
| #p #G #L #V #T #B #A #_ #_ #k #H destruct
| #p #G #L #V #T #B #A #_ #_ #k #H destruct
| #G #L #V #T #B #A #_ #_ #k #H destruct
#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
#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
| #p #G #L #V #T #B #A #HV #HT #q #W #U #H destruct /2 width=2 by ex2_intro/
| #p #G #L #V #T #B #A #_ #_ #q #W #U #H destruct
| #G #L #V #T #B #A #_ #_ #q #W #U #H destruct
| #p #G #L #V #T #B #A #HV #HT #q #W #U #H destruct /2 width=2 by ex2_intro/
| #p #G #L #V #T #B #A #_ #_ #q #W #U #H destruct
| #G #L #V #T #B #A #_ #_ #q #W #U #H destruct
#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
#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
| #p #G #L #V #T #B #A #_ #_ #q #W #U #H destruct
| #p #G #L #V #T #B #A #HV #HT #q #W #U #H destruct /2 width=5 by ex3_2_intro/
| #G #L #V #T #B #A #_ #_ #q #W #U #H destruct
| #p #G #L #V #T #B #A #_ #_ #q #W #U #H destruct
| #p #G #L #V #T #B #A #HV #HT #q #W #U #H destruct /2 width=5 by ex3_2_intro/
| #G #L #V #T #B #A #_ #_ #q #W #U #H destruct
#G #L #T #A * -G -L -T -A
[ #G #L #s #W #U #H destruct
| #I #G #L #V #B #_ #W #U #H destruct
#G #L #T #A * -G -L -T -A
[ #G #L #s #W #U #H destruct
| #I #G #L #V #B #_ #W #U #H destruct
| #p #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #p #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #G #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=3 by ex2_intro/
| #p #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #p #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #G #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=3 by ex2_intro/
∃∃B. ⦃G, L⦄ ⊢ V ⁝ B & ⦃G, L⦄ ⊢ T ⁝ ②B.A.
/2 width=3 by aaa_inv_appl_aux/ qed-.
∃∃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 →
+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
⦃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
| #p #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #p #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #p #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #p #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #G #L #V #T #B #A #_ #_ #W #U #H destruct
-lemma aaa_inv_cast: ∀G,L,W,T,A. ⦃G, L⦄ ⊢ ⓝW. 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-.
⦃G, L⦄ ⊢ W ⁝ A ∧ ⦃G, L⦄ ⊢ T ⁝ A.
/2 width=3 by aaa_inv_cast_aux/ qed-.