∀G,L1,L2. ⦃G,L1⦄ ⊢ ⬈[h,T2] L2 → ⦃G,L1⦄ ⊢ ⬈[h,T1] L2.
/2 width=5 by tdeq_rex_div/ qed-.
∀G,L1,L2. ⦃G,L1⦄ ⊢ ⬈[h,T2] L2 → ⦃G,L1⦄ ⊢ ⬈[h,T1] L2.
/2 width=5 by tdeq_rex_div/ qed-.
#h #G #L0 #T0 #T1 #H @(cpx_ind … H) -G -L0 -T0 -T1 /2 width=3 by ex2_intro/
[ #G #L0 #s0 #X0 #H0 #L1 #HL01 #L2 #HL02
elim (tdeq_inv_sort1 … H0) -H0 #s1 #H destruct
#h #G #L0 #T0 #T1 #H @(cpx_ind … H) -G -L0 -T0 -T1 /2 width=3 by ex2_intro/
[ #G #L0 #s0 #X0 #H0 #L1 #HL01 #L2 #HL02
elim (tdeq_inv_sort1 … H0) -H0 #s1 #H destruct
∀T2. T0 ≛ T2 →
∃∃T. T1 ≛ T & ⦃G,L⦄ ⊢ T2 ⬈[h] T.
#h #G #L #T0 #T1 #HT01 #T2 #HT02
∀T2. T0 ≛ T2 →
∃∃T. T1 ≛ T & ⦃G,L⦄ ⊢ T2 ⬈[h] T.
#h #G #L #T0 #T1 #HT01 #T2 #HT02
∀L2. L0 ≛[T0] L2 →
∃∃T. ⦃G,L2⦄ ⊢ T0 ⬈[h] T & T1 ≛ T.
#h #G #L0 #T0 #T1 #HT01 #L2 #HL02
∀L2. L0 ≛[T0] L2 →
∃∃T. ⦃G,L2⦄ ⊢ T0 ⬈[h] T & T1 ≛ T.
#h #G #L0 #T0 #T1 #HT01 #L2 #HL02
-/3 width=6 by rpx_fsge_comp, rdeq_fsge_comp, cpx_tdeq_conf_sex, rex_conf/ qed-.
+/3 width=6 by rpx_fsge_comp, rdeq_fsge_comp, cpx_tdeq_conf_rex, rex_conf/ qed-.
lemma rdeq_rpx_trans: ∀h,G,T,L2,K2. ⦃G,L2⦄ ⊢ ⬈[h,T] K2 →
∀L1. L1 ≛[T] L2 →
lemma rdeq_rpx_trans: ∀h,G,T,L2,K2. ⦃G,L2⦄ ⊢ ⬈[h,T] K2 →
∀L1. L1 ≛[T] L2 →