-lemma rsx_cpx_trans_jsx (h) (G):
- ∀L0,T1,T2. ❪G,L0❫ ⊢ T1 ⬈[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):
+ ∀L0,T1,T2. ❪G,L0❫ ⊢ T1 ⬈ T2 →
+ ∀L. G ⊢ L0 ⊒ L → G ⊢ ⬈*𝐒[T1] L → G ⊢ ⬈*𝐒[T2] L.
+#G #L0 #T1 #T2 #H @(cpx_ind … H) -G -L0 -T1 -T2