[ #d #e #J1 #K1 #W1 #i #H elim (ldrop_inv_atom1 … H) -H
#H destruct
| #I #L1 #L2 #V #HL12 #IHL12 #J1 #K1 #W1 #i #_ #_ #H elim (ylt_yle_false … H) //
[ #d #e #J1 #K1 #W1 #i #H elim (ldrop_inv_atom1 … H) -H
#H destruct
| #I #L1 #L2 #V #HL12 #IHL12 #J1 #K1 #W1 #i #_ #_ #H elim (ylt_yle_false … H) //
#IHL12 #J1 #K1 #W1 #i #H #_ elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ]
[ #_ lapply (ldrop_inv_O2 … H) -H
#H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_3_intro/
#IHL12 #J1 #K1 #W1 #i #H #_ elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ]
[ #_ lapply (ldrop_inv_O2 … H) -H
#H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_3_intro/