(* Basic_2A1: uses: lsx_cpx_trans_lcosx *)
lemma rsx_cpx_trans_jsx (G):
- â\88\80L0,T1,T2. â\9dªG,L0â\9d« ⊢ T1 ⬈ T2 →
+ â\88\80L0,T1,T2. â\9d¨G,L0â\9d© ⊢ T1 ⬈ T2 →
∀L. G ⊢ L0 ⊒ L → G ⊢ ⬈*𝐒[T1] L → G ⊢ ⬈*𝐒[T2] L.
#G #L0 #T1 #T2 #H @(cpx_ind … H) -G -L0 -T1 -T2
[ //
(* Basic_2A1: uses: lsx_cpx_trans_O *)
lemma rsx_cpx_trans (G):
- â\88\80L,T1,T2. â\9dªG,Lâ\9d« ⊢ T1 ⬈ T2 →
+ â\88\80L,T1,T2. â\9d¨G,Lâ\9d© ⊢ T1 ⬈ T2 →
G ⊢ ⬈*𝐒[T1] L → G ⊢ ⬈*𝐒[T2] L.
/3 width=6 by rsx_cpx_trans_jsx, jsx_refl/ qed-.
lemma rsx_cpxs_trans (G):
- â\88\80L,T1,T2. â\9dªG,Lâ\9d« ⊢ T1 ⬈* T2 →
+ â\88\80L,T1,T2. â\9d¨G,Lâ\9d© ⊢ T1 ⬈* T2 →
G ⊢ ⬈*𝐒[T1] L → G ⊢ ⬈*𝐒[T2] L.
#G #L #T1 #T2 #H
@(cpxs_ind_dx ??????? H) -T1 //