+lemma cpxs_tdeq_fpbs_trans: ∀h,G1,L1,T1,T. ⦃G1,L1⦄ ⊢ T1 ⬈*[h] T →
+ ∀T0. T ≛ T0 →
+ ∀G2,L2,T2. ⦃G1,L1,T0⦄ ≥[h] ⦃G2,L2,T2⦄ → ⦃G1,L1,T1⦄ ≥[h] ⦃G2,L2,T2⦄.
+/3 width=3 by cpxs_fpbs_trans, tdeq_fpbs_trans/ qed-.
+
+lemma cpxs_tdeq_fpbs: ∀h,G,L,T1,T. ⦃G,L⦄ ⊢ T1 ⬈*[h] T →
+ ∀T2. T ≛ T2 → ⦃G,L,T1⦄ ≥[h] ⦃G,L,T2⦄.
+/4 width=3 by cpxs_fpbs_trans, fdeq_fpbs, tdeq_fdeq/ qed.
+