-lemma rsx_cpx_trans_jsx (h) (G):
- ∀L0,T1,T2. ⦃G,L0⦄ ⊢ T1 ⬈[h] T2 →
- ∀f,L. G ⊢ L0 ⊒[h,f] 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