/4 width=2 by lsubsx_pair, rdsx_bind_void/
| #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #f #L #HL0 #HL
elim (rdsx_inv_flat … HL) -HL /3 width=2 by rdsx_flat/
/4 width=2 by lsubsx_pair, rdsx_bind_void/
| #I0 #G #L0 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #f #L #HL0 #HL
elim (rdsx_inv_flat … HL) -HL /3 width=2 by rdsx_flat/