[ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/
| lapply (ldrop_fwd_length_le2 … HLK2) -K2
lapply (lleq_fwd_length … HL12) -T -U //
[ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/
| lapply (ldrop_fwd_length_le2 … HLK2) -K2
lapply (lleq_fwd_length … HL12) -T -U //