-lemma cprs_fwd_beta_vector: ∀L,Vs,V,W,T,U. L ⊢ ⒶVs. ⓐV. ⓛW. T ➡* U →
- ⒶVs. ⓐV. ⓛW. T ≃ U ∨ L ⊢ ⒶVs. ⓓV. T ➡* U.
-#L #Vs elim Vs -Vs /2 width=1 by cprs_fwd_beta/
+lemma cprs_fwd_beta_vector: ∀a,L,Vs,V,W,T,U. L ⊢ ⒶVs. ⓐV. ⓛ{a}W. T ➡* U →
+ ⒶVs. ⓐV. ⓛ{a}W. T ≃ U ∨ L ⊢ ⒶVs. ⓓ{a}V. T ➡* U.
+#a #L #Vs elim Vs -Vs /2 width=1 by cprs_fwd_beta/