(* activate genv *)
inductive aaa: relation4 genv lenv term aarity ≝
| aaa_sort: ∀G,L,k. aaa G L (⋆k) (⓪)
(* activate genv *)
inductive aaa: relation4 genv lenv term aarity ≝
| aaa_sort: ∀G,L,k. aaa G L (⋆k) (⓪)
-| aaa_lref: ∀I,G,L,K,V,B,i. ⇩[0, i] L ≡ K. ⓑ{I}V → aaa G K V B → aaa G L (#i) B
+| aaa_lref: ∀I,G,L,K,V,B,i. ⇩[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 →
- ∃∃I,K,V. ⇩[0, i] L ≡ K.ⓑ{I} V & ⦃G, K⦄ ⊢ V ⁝ A.
+ ∃∃I,K,V. ⇩[i] L ≡ K.ⓑ{I} V & ⦃G, K⦄ ⊢ V ⁝ A.
| #a #G #L #V #T #B #A #_ #_ #i #H destruct
| #a #G #L #V #T #B #A #_ #_ #i #H destruct
| #G #L #V #T #B #A #_ #_ #i #H destruct
| #a #G #L #V #T #B #A #_ #_ #i #H destruct
| #a #G #L #V #T #B #A #_ #_ #i #H destruct
| #G #L #V #T #B #A #_ #_ #i #H destruct
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 →
- ∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & ⦃G, K⦄ ⊢ V ⁝ A.
+ ∃∃I,K,V. ⇩[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 → ⊥.
#G #L #T #A * -G -L -T -A
[ #G #L #k #a #W #U #H destruct
| #I #G #L #K #V #B #i #_ #_ #a #W #U #H destruct
#G #L #T #A * -G -L -T -A
[ #G #L #k #a #W #U #H destruct
| #I #G #L #K #V #B #i #_ #_ #a #W #U #H destruct
| #b #G #L #V #T #B #A #_ #_ #a #W #U #H destruct
| #G #L #V #T #B #A #_ #_ #a #W #U #H destruct
| #G #L #V #T #A #_ #_ #a #W #U #H destruct
| #b #G #L #V #T #B #A #_ #_ #a #W #U #H destruct
| #G #L #V #T #B #A #_ #_ #a #W #U #H destruct
| #G #L #V #T #A #_ #_ #a #W #U #H destruct
[ #G #L #k #a #W #U #H destruct
| #I #G #L #K #V #B #i #_ #_ #a #W #U #H destruct
| #b #G #L #V #T #B #A #_ #_ #a #W #U #H destruct
[ #G #L #k #a #W #U #H destruct
| #I #G #L #K #V #B #i #_ #_ #a #W #U #H destruct
| #b #G #L #V #T #B #A #_ #_ #a #W #U #H destruct
| #I #G #L #K #V #B #i #_ #_ #W #U #H destruct
| #a #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #a #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #I #G #L #K #V #B #i #_ #_ #W #U #H destruct
| #a #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #a #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #a #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #a #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #a #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #a #G #L #V #T #B #A #_ #_ #W #U #H destruct
| #G #L #V #T #B #A #_ #_ #W #U #H destruct