-lemma cpxs_fwd_theta: ∀h,o,p,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}V.T ⬈*[h] U →
- ∀V2. ⬆*[1] V1 ≘ V2 → ⓐV1.ⓓ{p}V.T ⩳[h, o] U ∨
- â¦\83G, Lâ¦\84 â\8a¢ â\93\93{p}V.â\93\90V2.T â¬\88*[h] U.
-#h #o #p #G #L #V1 #V #T #U #H #V2 #HV12
+lemma cpxs_fwd_theta: ∀h,p,G,L,V1,V,T,X2. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{p}V.T ⬈*[h] X2 →
+ ∀V2. ⬆*[1] V1 ≘ V2 →
+ â\88¨â\88¨ â\93\90V1.â\93\93{p}V.T ⩳ X2 | â¦\83G, Lâ¦\84 â\8a¢ â\93\93{p}V.â\93\90V2.T â¬\88*[h] X2.
+#h #p #G #L #V1 #V #T #X2 #H #V2 #HV12