-lemma csn_applv_beta: ∀L,W. L ⊢ ⬊* W →
- ∀Vs,V,T. L ⊢ ⬊* ⒶVs.ⓓV.T →
- L ⊢ ⬊* ⒶVs. ⓐV.ⓛW. T.
-#L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW
+lemma csn_applv_beta: ∀a,L,W. L ⊢ ⬊* W →
+ ∀Vs,V,T. L ⊢ ⬊* ⒶVs.ⓓ{a}V.T →
+ L ⊢ ⬊* ⒶVs. ⓐV.ⓛ{a}W. T.
+#a #L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW