-lemma llpx_sn_inv_lift_le: ∀R. l_deliftable_sn R →
- ∀L1,L2,U,d0. llpx_sn R d0 U L1 L2 →
- ∀K1,K2,d,e. ⬇[Ⓕ, d, e] L1 ≡ K1 → ⬇[Ⓕ, d, e] L2 ≡ K2 →
- ∀T. ⬆[d, e] T ≡ U → d0 ≤ d → llpx_sn R d0 T K1 K2.
-#R #HR #L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0
-[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X
- lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d -e
+lemma llpx_sn_inv_lift_le: ∀R. d_deliftable_sn R →
+ ∀L1,L2,U,l0. llpx_sn R l0 U L1 L2 →
+ ∀K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 →
+ ∀T. ⬆[l, m] T ≡ U → l0 ≤ l → llpx_sn R l0 T K1 K2.
+#R #HR #L1 #L2 #U #l0 #H elim H -L1 -L2 -U -l0
+[ #L1 #L2 #l0 #k #HL12 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X
+ lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l -m