-lemma cpxs_fwd_cast_vector (h) (G) (L):
- ∀Vs,W,T,X2. ❪G,L❫ ⊢ ⒶVs.ⓝW.T ⬈*[h] X2 →
- ∨∨ ⒶVs. ⓝW. T ⩳ X2
- | ❪G,L❫ ⊢ ⒶVs.T ⬈*[h] X2
- | ❪G,L❫ ⊢ ⒶVs.W ⬈*[h] X2.
-#h #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/
+lemma cpxs_fwd_cast_vector (G) (L):
+ ∀Vs,W,T,X2. ❪G,L❫ ⊢ ⒶVs.ⓝW.T ⬈* X2 →
+ ∨∨ ⒶVs. ⓝW. T ~ X2
+ | ❪G,L❫ ⊢ ⒶVs.T ⬈* X2
+ | ❪G,L❫ ⊢ ⒶVs.W ⬈* X2.
+#G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/