-lemma rsx_cpx_trans_jsx (h) (G):
- â\88\80L0,T1,T2. â¦\83G,L0â¦\84 â\8a¢ T1 â¬\88[h] T2 →
- ∀L. G ⊢ L0 ⊒[h] L → G ⊢ ⬈*[h,T1] 𝐒⦃L⦄ → G ⊢ ⬈*[h,T2] 𝐒⦃L⦄.
-#h #G #L0 #T1 #T2 #H @(cpx_ind … H) -G -L0 -T1 -T2
+lemma rsx_cpx_trans_jsx (G):
+ â\88\80L0,T1,T2. â\9dªG,L0â\9d« â\8a¢ T1 â¬\88 T2 →
+ ∀L. G ⊢ L0 ⊒ L → G ⊢ ⬈*𝐒[T1] L → G ⊢ ⬈*𝐒[T2] L.
+#G #L0 #T1 #T2 #H @(cpx_ind … H) -G -L0 -T1 -T2