include "basic_2/notation/relations/atomicarity_4.ma".
include "basic_2/grammar/aarity.ma".
include "basic_2/grammar/genv.ma".
include "basic_2/notation/relations/atomicarity_4.ma".
include "basic_2/grammar/aarity.ma".
include "basic_2/grammar/genv.ma".
(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
(* activate genv *)
inductive aaa: relation4 genv lenv term aarity ≝
| aaa_sort: ∀G,L,k. aaa G L (⋆k) (⓪)
(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
(* activate genv *)
inductive aaa: relation4 genv lenv term aarity ≝
| aaa_sort: ∀G,L,k. aaa G L (⋆k) (⓪)
-| aaa_lref: â\88\80I,G,L,K,V,B,i. â\87©[i] L ≡ K. ⓑ{I}V → aaa G K V B → aaa G L (#i) B
+| aaa_lref: â\88\80I,G,L,K,V,B,i. â¬\87[i] L ≡ K. ⓑ{I}V → aaa G K V B → aaa G L (#i) B
| aaa_abbr: ∀a,G,L,V,T,B,A.
aaa G L V B → aaa G (L.ⓓV) T A → aaa G L (ⓓ{a}V.T) A
| aaa_abst: ∀a,G,L,V,T,B,A.
| aaa_abbr: ∀a,G,L,V,T,B,A.
aaa G L V B → aaa G (L.ⓓV) T A → aaa G L (ⓓ{a}V.T) A
| aaa_abst: ∀a,G,L,V,T,B,A.
/2 width=6 by aaa_inv_sort_aux/ qed-.
fact aaa_inv_lref_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀i. T = #i →
/2 width=6 by aaa_inv_sort_aux/ qed-.
fact aaa_inv_lref_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀i. T = #i →
- â\88\83â\88\83I,K,V. â\87©[i] L ≡ K.ⓑ{I} V & ⦃G, K⦄ ⊢ V ⁝ A.
+ â\88\83â\88\83I,K,V. â¬\87[i] L ≡ K.ⓑ{I} V & ⦃G, K⦄ ⊢ V ⁝ A.
#G #L #T #A * -G -L -T -A
[ #G #L #k #i #H destruct
| #I #G #L #K #V #B #j #HLK #HB #i #H destruct /2 width=5 by ex2_3_intro/
#G #L #T #A * -G -L -T -A
[ #G #L #k #i #H destruct
| #I #G #L #K #V #B #j #HLK #HB #i #H destruct /2 width=5 by ex2_3_intro/
qed-.
lemma aaa_inv_lref: ∀G,L,A,i. ⦃G, L⦄ ⊢ #i ⁝ A →
qed-.
lemma aaa_inv_lref: ∀G,L,A,i. ⦃G, L⦄ ⊢ #i ⁝ A →
- â\88\83â\88\83I,K,V. â\87©[i] L ≡ K. ⓑ{I} V & ⦃G, K⦄ ⊢ V ⁝ A.
+ â\88\83â\88\83I,K,V. â¬\87[i] L ≡ K. ⓑ{I} V & ⦃G, K⦄ ⊢ V ⁝ A.
/2 width=3 by aaa_inv_lref_aux/ qed-.
fact aaa_inv_gref_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀p. T = §p → ⊥.
/2 width=3 by aaa_inv_lref_aux/ qed-.
fact aaa_inv_gref_aux: ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ∀p. T = §p → ⊥.