-(* Basic_2A1: includes: lpr_fpb *)
-lemma lfpr_fpb: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) →
- ⦃G, L1, T⦄ ≻[h, o] ⦃G, L2, T⦄.
-/3 width=1 by fpb_lfpx, lfpr_fwd_lfpx/ qed.
+lemma lpr_fpb (h) (G) (T): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → (L1 ≛[T] L2 → ⊥) →
+ ⦃G, L1, T⦄ ≻[h] ⦃G, L2, T⦄.
+/3 width=1 by fpb_lpx, lpr_fwd_lpx/ qed.