elim (IHT1 … T0) -IHT1
[ #T2 #n2 * #HT02 #HT2 /4 width=5 by cpms_trans, cpmuwe_intro, ex1_2_intro/
| /3 width=1 by teqx_tweq/
elim (IHT1 … T0) -IHT1
[ #T2 #n2 * #HT02 #HT2 /4 width=5 by cpms_trans, cpmuwe_intro, ex1_2_intro/
| /3 width=1 by teqx_tweq/