[ elim (tdeq_dec h o T T2) #H2T2
[ -IH -IH2 -IH1 -H0T1 /4 width=7 by tdeq_trans, ex4_3_intro/
| lapply (cnv_cpm_trans_lpr_aux … IH2 IH1 … H1T1 L ?) [6:|*: // ] -H1T2 -H2T12 #H0T
- elim (IH H0T H2T2) [|*: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ] -IH -IH2 -H0T -H2T2
+ elim (IH H0T H2T2) [|*: /4 width=5 by cpm_fpbq, fpbq_fpbg_trans/ ] -IH -IH2 -H0T -H2T2 (**)
#m1 #m2 #T0 #H1T0 #H2T0 #H1T02 #H destruct
elim (cnv_cpm_tdeq_cpm_trans_aux … IH1 … H0T1 … H1T1 H2T1 … H1T0) -IH1 -H0T1 -H1T1 -H1T0
#T3 #H1T13 #H1T30 #H2T30
elim (tdeq_dec h o T1 T) #H2T1
[ lapply (cnv_cpm_trans_lpr_aux … IH2 IH1 … H1T1 L ?) [6:|*: // ] #H0T
lapply (tdeq_canc_sn … H2T1 … H2T12) -H2T12 #H2T2
- /6 width=7 by cpm_fpbq, fpbq_fpbg_trans/
+ /6 width=7 by cpm_fpbq, fpbq_fpbg_trans/ (**)
| -IB2 -IH -IH2 -IH1
elim (cnv_fpbg_refl_false … o … H0T1) -a -Q
/3 width=8 by cpm_tdneq_cpm_cpms_tdeq_sym_fwd_fpbg/