#H3 #H4 /2 width=3 by fqu_bind_dx, ex2_intro/
| #I #G #L2 #V #T #L1 #H elim (lleq_inv_flat … H) -H
/2 width=3 by fqu_flat_dx, ex2_intro/
-| #G #L2 #K2 #T #U #e #HLK2 #HTU #L1 #HL12
- elim (drop_O1_le (Ⓕ) (e+1) L1)
+| #G #L2 #K2 #T #U #m #HLK2 #HTU #L1 #HL12
+ elim (drop_O1_le (Ⓕ) (m+1) L1)
[ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/
| lapply (drop_fwd_length_le2 … HLK2) -K2
lapply (lleq_fwd_length … HL12) -T -U //