-fact leq_lpxs_trans_lleq_aux: ∀h,g,G,L1,L0,d,e. L1 ⩬[d, e] L0 → e = ∞ →
- ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 →
- ∃∃L. L ⩬[d, e] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L &
- (∀T. L0 ≡[T, d] L2 ↔ L1 ≡[T, d] L).
-#h #g #G #L1 #L0 #d #e #H elim H -L1 -L0 -d -e
-[ #d #e #_ #L2 #H >(lpxs_inv_atom1 … H) -H
+fact lreq_lpxs_trans_lleq_aux: ∀h,g,G,L1,L0,l,m. L1 ⩬[l, m] L0 → m = ∞ →
+ ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 →
+ ∃∃L. L ⩬[l, m] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L &
+ (∀T. L0 ≡[T, l] L2 ↔ L1 ≡[T, l] L).
+#h #g #G #L1 #L0 #l #m #H elim H -L1 -L0 -l -m
+[ #l #m #_ #L2 #H >(lpxs_inv_atom1 … H) -H