- elim (cnv_inv_appl_true_cpes … H) -H #q #W0 #U0 #_ #_ #_ #HTU0
- elim (cnv_cpme_cpms_conf … HT … HTU0 … HTX) -T #HX #_
- elim (cpms_inv_abst_sn … HX) -HX #V0 #T0 #_ #_ #H destruct -W0 -U0
- /2 width=4 by/
- ]
- | elim (cpue_total_csx h G L T)
- [| /3 width=2 by cnv_fwd_fsb, fsb_inv_csx/ ] #X
- elim (abst_dec X) [ * ]
- [ #p #W #U #H #HTU destruct
- elim (cnv_cpes_dec … 1 0 … HV W) [ #HVW | #HnVW ]
- [ elim HTU -HTU #n #HTU #_
- @or_introl @(cnv_appl_cpes … HV … HT … HVW … HTU) #H destruct
- | @or_intror #H
- elim (cnv_inv_appl_cpes … H) -H #m1 #q #W0 #U0 #_ #_ #_ #HVW0 #HTU0
- elim (cnv_cpue_cpms_conf … HT … HTU0 … HTU) -m1 -T #X * #m2 #HU0X #_ #HUX
- elim (tueq_inv_bind1 … HUX) -HUX #X0 #_ #H destruct -U
- elim (cpms_inv_abst_bi … HU0X) -HU0X #_ #HW0 #_ -p -q -m2 -U0 -X0
- /3 width=3 by cpes_cprs_trans/
- | lapply (cnv_cpue_trans … HT … HTU) -T #H
- elim (cnv_inv_bind … H) -H #HW #_ //
- ]
- | #HnTU #HTX
- @or_intror #H
- elim (cnv_inv_appl_cpes … H) -H #m1 #q #W0 #U0 #_ #_ #_ #_ #HTU0
- elim (cnv_cpue_cpms_conf … HT … HTU0 … HTX) -m1 -T #X0 * #m2 #HUX0 #_ #HX0
- elim (cpms_inv_abst_sn … HUX0) -HUX0 #V0 #T0 #_ #_ #H destruct -m2 -W0 -U0
- elim (tueq_inv_bind2 … HX0) -HX0 #X0 #_ #H destruct
+ elim (cnv_inv_appl_cpes … H) -H #m0 #q #W0 #U0 #_ #_ #_ #_ #HTU0
+ lapply (cpmuwe_abst … HTU0) -HTU0 #HTU0
+ elim (cnv_cpmuwe_mono … HT … HTU0 … HX0) -T #_ #H
+ elim (tweq_inv_abst_sn … H) -W0 -U0 #W0 #U0 #H destruct