#G #L2 #T1 #T2 #H @(cpx_ind … H) -G -L2 -T1 -T2 /2 width=2 by cpx_qu/
[ #I #G #K2 #V1 #V2 #W2 #_ #IH #HVW2 #L1 #H
elim (req_inv_zero_pair_dx … H) -H #K1 #HK12 #H destruct
#G #L2 #T1 #T2 #H @(cpx_ind … H) -G -L2 -T1 -T2 /2 width=2 by cpx_qu/
[ #I #G #K2 #V1 #V2 #W2 #_ #IH #HVW2 #L1 #H
elim (req_inv_zero_pair_dx … H) -H #K1 #HK12 #H destruct