-lemma cprs_fpbc: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⊥) →
- ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄.
-/3 width=1 by fpbc_cpxs, cprs_cpxs/ qed.
-
-lemma lprs_fpbc: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → (L1 ⋕[0, T] L2 → ⊥) →
- ⦃G, L1, T⦄ ≻[h, g] ⦃G, L2, T⦄.
-/3 width=1 by fpbc_lpxs, lprs_lpxs/ qed.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma fpbc_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ →
- ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
-/3 width=1 by lpxs_fpbs, cpxs_fpbs, fqup_fpbs/
-qed-.
+lemma fpbu_fpbc: ∀h,g,G1,G2,L1,L2,T1,T2.
+ ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≻⋕[h, g] ⦃G2, L2, T2⦄.
+/2 width=5 by ex2_3_intro/ qed.