- elim (IH … HK12) -K1 /3 width=5 by lsubc_pair, drops_skip, ex2_intro/
- | #K2 #V #W2 #A #HV #H1W2 #H2W2 #HK12 #H1 #H2 #H3 destruct
+ elim (IH … HK12) -K1 /3 width=5 by lsubc_bind, drops_skip, ex2_intro/
+ | #K2 #V2 #W2 #A #HV2 #H1W2 #H2W2 #HK12 #H1 #H2 destruct
+ elim (liftsb_inv_pair_sn … HZ) -HZ #V1 #HV21 #H destruct