-| 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)