elim (lsubd_inv_pair2 … H) -H * #K1 [ | -IHV -HLK1 ]
[ #HK12 #H destruct /3 width=4/
| #W #l0 #_ #_ #_ #H destruct
]
| #G #L2 #K2 #W #i #l #HLK2 #HW #IHW #L1 #HL12
elim (lsubd_inv_pair2 … H) -H * #K1 [ | -IHV -HLK1 ]
[ #HK12 #H destruct /3 width=4/
| #W #l0 #_ #_ #_ #H destruct
]
| #G #L2 #K2 #W #i #l #HLK2 #HW #IHW #L1 #HL12