elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
lapply (aaa_cprs_conf … HA1 … HT1) -T1 #HA1
lapply (aaa_cprs_conf … HA2 … HT2) -T2 #HA2
elim (cpcs_inv_cprs … HT12) -HT12 #T #HT1 #HT2
lapply (aaa_cprs_conf … HA1 … HT1) -T1 #HA1
lapply (aaa_cprs_conf … HA2 … HT2) -T2 #HA2