-lemma cpxs_fwd_cast_vector (h) (G) (L):
- â\88\80Vs,W,T,X2. â\9dªG,Lâ\9d« â\8a¢ â\92¶Vs.â\93\9dW.T â¬\88*[h] X2 →
- ∨∨ ⒶVs. ⓝW. T ⩳ X2
- | â\9dªG,Lâ\9d« â\8a¢ â\92¶Vs.T â¬\88*[h] X2
- | â\9dªG,Lâ\9d« â\8a¢ â\92¶Vs.W â¬\88*[h] X2.
-#h #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/
+lemma cpxs_fwd_cast_vector (G) (L):
+ â\88\80Vs,W,T,X2. â\9d¨G,Lâ\9d© â\8a¢ â\92¶Vs.â\93\9dW.T â¬\88* X2 →
+ ∨∨ ⒶVs. ⓝW. T ~ X2
+ | â\9d¨G,Lâ\9d© â\8a¢ â\92¶Vs.T â¬\88* X2
+ | â\9d¨G,Lâ\9d© â\8a¢ â\92¶Vs.W â¬\88* X2.
+#G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/