inductive aaa: lenv → term → predicate aarity ≝
| aaa_sort: ∀L,k. aaa L (⋆k) ⓪
| aaa_lref: ∀I,L,K,V,B,i. ⇩[0, i] L ≡ K. ⓑ{I} V → aaa K V B → aaa L (#i) B
-| aaa_abbr: ∀L,V,T,B,A.
- aaa L V B → aaa (L. ⓓV) T A → aaa L (ⓓV. T) A
-| aaa_abst: ∀L,V,T,B,A.
- aaa L V B → aaa (L. ⓛV) T A → aaa L (ⓛV. T) (②B. A)
+| aaa_abbr: ∀a,L,V,T,B,A.
+ aaa L V B → aaa (L. ⓓV) T A → aaa L (ⓓ{a}V. T) A
+| aaa_abst: ∀a,L,V,T,B,A.
+ aaa L V B → aaa (L. ⓛV) T A → aaa L (ⓛ{a}V. T) (②B. A)
| aaa_appl: ∀L,V,T,B,A. aaa L V B → aaa L T (②B. A) → aaa L (ⓐV. T) A
| aaa_cast: ∀L,V,T,A. aaa L V A → aaa L T A → aaa L (ⓝV. T) A
.
#L #T #A * -L -T -A
[ //
| #I #L #K #V #B #i #_ #_ #k #H destruct
-| #L #V #T #B #A #_ #_ #k #H destruct
-| #L #V #T #B #A #_ #_ #k #H destruct
+| #a #L #V #T #B #A #_ #_ #k #H destruct
+| #a #L #V #T #B #A #_ #_ #k #H destruct
| #L #V #T #B #A #_ #_ #k #H destruct
| #L #V #T #A #_ #_ #k #H destruct
]
#L #T #A * -L -T -A
[ #L #k #i #H destruct
| #I #L #K #V #B #j #HLK #HB #i #H destruct /2 width=5/
-| #L #V #T #B #A #_ #_ #i #H destruct
-| #L #V #T #B #A #_ #_ #i #H destruct
+| #a #L #V #T #B #A #_ #_ #i #H destruct
+| #a #L #V #T #B #A #_ #_ #i #H destruct
| #L #V #T #B #A #_ #_ #i #H destruct
| #L #V #T #A #_ #_ #i #H destruct
]
∃∃I,K,V. ⇩[0, i] L ≡ K. ⓑ{I} V & K ⊢ V ⁝ A.
/2 width=3/ qed-.
-fact aaa_inv_abbr_aux: ∀L,T,A. L ⊢ T ⁝ A → ∀W,U. T = ⓓW. U →
+fact aaa_inv_abbr_aux: ∀L,T,A. L ⊢ T ⁝ A → ∀a,W,U. T = ⓓ{a}W. U →
∃∃B. L ⊢ W ⁝ B & L. ⓓW ⊢ U ⁝ A.
#L #T #A * -L -T -A
-[ #L #k #W #U #H destruct
-| #I #L #K #V #B #i #_ #_ #W #U #H destruct
-| #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=2/
-| #L #V #T #B #A #_ #_ #W #U #H destruct
-| #L #V #T #B #A #_ #_ #W #U #H destruct
-| #L #V #T #A #_ #_ #W #U #H destruct
+[ #L #k #a #W #U #H destruct
+| #I #L #K #V #B #i #_ #_ #a #W #U #H destruct
+| #b #L #V #T #B #A #HV #HT #a #W #U #H destruct /2 width=2/
+| #b #L #V #T #B #A #_ #_ #a #W #U #H destruct
+| #L #V #T #B #A #_ #_ #a #W #U #H destruct
+| #L #V #T #A #_ #_ #a #W #U #H destruct
]
qed.
-lemma aaa_inv_abbr: ∀L,V,T,A. L ⊢ ⓓV. T ⁝ A →
+lemma aaa_inv_abbr: ∀a,L,V,T,A. L ⊢ ⓓ{a}V. T ⁝ A →
∃∃B. L ⊢ V ⁝ B & L. ⓓV ⊢ T ⁝ A.
-/2 width=3/ qed-.
+/2 width=4/ qed-.
-fact aaa_inv_abst_aux: ∀L,T,A. L ⊢ T ⁝ A → ∀W,U. T = ⓛW. U →
+fact aaa_inv_abst_aux: ∀L,T,A. L ⊢ T ⁝ A → ∀a,W,U. T = ⓛ{a}W. U →
∃∃B1,B2. L ⊢ W ⁝ B1 & L. ⓛW ⊢ U ⁝ B2 & A = ②B1. B2.
#L #T #A * -L -T -A
-[ #L #k #W #U #H destruct
-| #I #L #K #V #B #i #_ #_ #W #U #H destruct
-| #L #V #T #B #A #_ #_ #W #U #H destruct
-| #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=5/
-| #L #V #T #B #A #_ #_ #W #U #H destruct
-| #L #V #T #A #_ #_ #W #U #H destruct
+[ #L #k #a #W #U #H destruct
+| #I #L #K #V #B #i #_ #_ #a #W #U #H destruct
+| #b #L #V #T #B #A #_ #_ #a #W #U #H destruct
+| #b #L #V #T #B #A #HV #HT #a #W #U #H destruct /2 width=5/
+| #L #V #T #B #A #_ #_ #a #W #U #H destruct
+| #L #V #T #A #_ #_ #a #W #U #H destruct
]
qed.
-lemma aaa_inv_abst: ∀L,W,T,A. L ⊢ ⓛW. T ⁝ A →
+lemma aaa_inv_abst: ∀a,L,W,T,A. L ⊢ ⓛ{a}W. T ⁝ A →
∃∃B1,B2. L ⊢ W ⁝ B1 & L. ⓛW ⊢ T ⁝ B2 & A = ②B1. B2.
-/2 width=3/ qed-.
+/2 width=4/ qed-.
fact aaa_inv_appl_aux: ∀L,T,A. L ⊢ T ⁝ A → ∀W,U. T = ⓐW. U →
∃∃B. L ⊢ W ⁝ B & L ⊢ U ⁝ ②B. A.
#L #T #A * -L -T -A
[ #L #k #W #U #H destruct
| #I #L #K #V #B #i #_ #_ #W #U #H destruct
-| #L #V #T #B #A #_ #_ #W #U #H destruct
-| #L #V #T #B #A #_ #_ #W #U #H destruct
+| #a #L #V #T #B #A #_ #_ #W #U #H destruct
+| #a #L #V #T #B #A #_ #_ #W #U #H destruct
| #L #V #T #B #A #HV #HT #W #U #H destruct /2 width=3/
| #L #V #T #A #_ #_ #W #U #H destruct
]
#L #T #A * -L -T -A
[ #L #k #W #U #H destruct
| #I #L #K #V #B #i #_ #_ #W #U #H destruct
-| #L #V #T #B #A #_ #_ #W #U #H destruct
-| #L #V #T #B #A #_ #_ #W #U #H destruct
+| #a #L #V #T #B #A #_ #_ #W #U #H destruct
+| #a #L #V #T #B #A #_ #_ #W #U #H destruct
| #L #V #T #B #A #_ #_ #W #U #H destruct
| #L #V #T #A #HV #HT #W #U #H destruct /2 width=1/
]