| aaa_abst: ∀L,V,T,B,A.
aaa L V B → aaa (L. ⓛV) T A → aaa L (ⓛ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: â\88\80L,V,T,A. aaa L V A â\86\92 aaa L T A â\86\92 aaa L (â\93£V. T) A
+| aaa_cast: â\88\80L,V,T,A. aaa L V A â\86\92 aaa L T A â\86\92 aaa L (â\93\9dV. T) A
.
interpretation "atomic arity assignment (term)"
∃∃B. L ⊢ V ⁝ B & L ⊢ T ⁝ ②B. A.
/2 width=3/ qed-.
-fact aaa_inv_cast_aux: â\88\80L,T,A. L â\8a¢ T â\81\9d A â\86\92 â\88\80W,U. T = â\93£W. U →
+fact aaa_inv_cast_aux: â\88\80L,T,A. L â\8a¢ T â\81\9d A â\86\92 â\88\80W,U. T = â\93\9dW. U →
L ⊢ W ⁝ A ∧ L ⊢ U ⁝ A.
#L #T #A * -L -T -A
[ #L #k #W #U #H destruct
]
qed.
-lemma aaa_inv_cast: â\88\80L,W,T,A. L â\8a¢ â\93£W. T ⁝ A →
+lemma aaa_inv_cast: â\88\80L,W,T,A. L â\8a¢ â\93\9dW. T ⁝ A →
L ⊢ W ⁝ A ∧ L ⊢ T ⁝ A.
/2 width=3/ qed-.