| #g #Hg #HLK1 #H destruct -HL12
elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
]
| #L1 #L2 #W #V #A #HV #HW #HL12 #IH #b #f #K1 #Hf #H
| #g #Hg #HLK1 #H destruct -HL12
elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
]
| #L1 #L2 #W #V #A #HV #HW #HL12 #IH #b #f #K1 #Hf #H