-lemma tdeq_fpbs_trans: ∀h,o,T1,T. T1 ≛[h, o] T →
- ∀G1,G2,L1,L2,T2. ⦃G1, L1, T⦄ ≥[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, o] ⦃G2, L2, T2⦄.
-/3 width=5 by ffdeq_fpbs_trans, tdeq_ffdeq/ qed-.
+lemma teqx_fpbs_trans:
+ ∀T1,T. T1 ≅ T →
+ ∀G1,G2,L1,L2,T2. ❪G1,L1,T❫ ≥ ❪G2,L2,T2❫ → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
+/3 width=5 by feqx_fpbs_trans, teqg_feqg/ qed-.
+
+lemma fpbs_teqx_trans:
+ ∀G1,G2,L1,L2,T1,T. ❪G1,L1,T1❫ ≥ ❪G2,L2,T❫ →
+ ∀T2. T ≅ T2 → ❪G1,L1,T1❫ ≥ ❪G2,L2,T2❫.
+/3 width=5 by fpbs_feqx_trans, teqg_feqg/ qed-.