-lemma cpxs_fwd_cast: ∀h,g,L,W,T,U. ⦃h, L⦄ ⊢ ⓝW.T ➡*[g] U →
- ∨∨ ⓝW. T ≃ U | ⦃h, L⦄ ⊢ T ➡*[g] U | ⦃h, L⦄ ⊢ W ➡*[g] U.
-#h #g #L #W #T #U #H
-elim (cpxs_inv_cast1 … H) -H /2 width=1/ *
-#W0 #T0 #_ #_ #H destruct /2 width=1/
+lemma cpxs_fwd_cast: ∀h,g,G,L,W,T,U. ⦃G, L⦄ ⊢ ⓝW.T ➡*[h, g] U →
+ ∨∨ ⓝW. T ≃ U | ⦃G, L⦄ ⊢ T ➡*[h, g] U | ⦃G, L⦄ ⊢ W ➡*[h, g] U.
+#h #g #G #L #W #T #U #H
+elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ *
+#W0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or3_intro0/