-lemma lpxs_rdneq_fpbg: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h] L2 →
- (L1 ≛[h, o, T] L2 → ⊥) → ⦃G, L1, T⦄ >[h, o] ⦃G, L2, T⦄.
-#h #o #G #L1 #L2 #T #H #H0
+lemma lpxs_rdneq_fpbg: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h] L2 →
+ (L1 ≛[T] L2 → ⊥) → ⦃G, L1, T⦄ >[h] ⦃G, L2, T⦄.
+#h #G #L1 #L2 #T #H #H0