#h #n #G #L #T0 #T1 * #T #HT1 #HT0 #T2 #HT02
elim (cprs_conf … HT0 … HT02) -T0 #T0 #HT0 #HT20
/3 width=3 by cpms_div, cpms_cprs_trans/
#h #n #G #L #T0 #T1 * #T #HT1 #HT0 #T2 #HT02
elim (cprs_conf … HT0 … HT02) -T0 #T0 #HT0 #HT20
/3 width=3 by cpms_div, cpms_cprs_trans/