+(* Advanced properties ******************************************************)
+
+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, teqx_feqx/ 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, teqx_feqx/ qed-.
+