| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H
/2 width=4 by fqu_flat_dx, ex3_intro/
| #G1 #L1 #L #T1 #U1 #e #HL1 #HTU1 #K1 #H1KL1 #H2KL1
- elim (ldrop_O1_le (e+1) K1)
+ elim (ldrop_O1_le (Ⓕ) (e+1) K1)
[ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 //
#H2KL elim (lpxs_ldrop_trans_O1 … H1KL1 … HL1) -L1
#K0 #HK10 #H1KL lapply (ldrop_mono … HK10 … HK1) -HK10 #H destruct