elim (IH … HK12 … Hg) -IH -HK12 -Hg
[1,3: /3 width=5 by sex_next, sex_push, ex2_intro/
|2,4: /3 width=3 by drops_drop/
]
| elim (sex_inv_next1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct
elim (IH … HK12 … Hg) -IH -HK12 -Hg
[1,3: /3 width=5 by sex_next, sex_push, ex2_intro/
|2,4: /3 width=3 by drops_drop/
]
| elim (sex_inv_next1 … H) -H #I2 #K2 #HK12 #HI12 #H destruct