-| #T1 #T0 #HT10 #HT02 #IH #Hn12
- elim (teqx_dec T1 T0) [ -HT10 -HT02 #H10 | -IH #Hn10 ]
- [ elim IH -IH /3 width=3 by teqx_trans/ -Hn12
- #T3 #T4 #HT03 #Hn03 #HT34 #H42
- elim (teqx_cpx_trans … H10 … HT03) -HT03 #T5 #HT15 #H53
- elim (teqx_cpxs_trans … H53 … HT34) -HT34 #T6 #HT56 #H64
- /5 width=8 by teqx_canc_sn, (* 2x *) teqx_trans, ex4_2_intro/
- | /3 width=6 by ex4_2_intro/
+| #T1 #T0 #HT10 #HT02 #IH #HnT12
+ elim (teqx_dec T1 T0) [ -HT10 -HT02 #HT10 | -IH #HnT10 ]
+ [ elim IH -IH /3 width=3 by teqx_trans/ -HnT12
+ #T #HT0 #HnT0 #HT2
+ lapply (teqx_cpx_trans … HT10 … HT0) -HT0 #HT1
+ /4 width=4 by teqx_canc_sn, ex3_intro/
+ | /3 width=4 by ex3_intro/