[ #H elim H -H //
| #HV0 @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10
@(IHV … HLV0 … HV0) -HV0 /4 width=5 by csx_cpx_trans, cpx_pair_sn/ (**) (* full auto too slow *)
[ #H elim H -H //
| #HV0 @(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10
@(IHV … HLV0 … HV0) -HV0 /4 width=5 by csx_cpx_trans, cpx_pair_sn/ (**) (* full auto too slow *)