- elim (lstas_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct
- elim (cpds_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW20 #_ #H destruct
- lapply (cprs_div … HW10 … HW20) -W0 #HW12
- lapply (da_sta_conf … HVW1 … Hl0) <minus_plus_m_m #H
- elim (snv_fwd_da … HW2) #l #Hl
- lapply (IH4 … HV1 … 1 … Hl0 W1 ?) /2 width=1 by fqup_fpbg, sta_lstas/ #HW1
- lapply (da_cpcs_aux … IH3 IH2 … H … Hl … HW12) // -H
- /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, sta_fpbs/ #H destruct
- lapply (IH3 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
- lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2l
- elim (IH1 … 1 … Hl0 … W1 … HV12 … HL12) /2 width=1 by fqup_fpbg, sta_lstas/ -HVW1 #W4 #H #HW14
- lapply (lstas_inv_SO … H) #HV2W4
- lapply (da_sta_conf … HV2W4 … HV2l) <minus_plus_m_m #HW4l
- lapply (IH4 … HV2 … HV2l … H) -H /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs/ #HW4
+ elim (lstas_inv_bind1 … HT1U) -HT1U #U #HT2U #H destruct
+ elim (cpds_inv_abst1 … HTU1) -HTU1 #W0 #U0 #HW20 #_ #H destruct -U0 -l0
+ elim (snv_fwd_da … HW2) #l0 #HW2l
+ lapply (cpds_div … W2 … 0 … HVW1) /2 width=3 by cprs_cpds/ -W0 #H21
+ elim (snv_fwd_da … HV1) #l #HV1l
+ elim (da_cpes_aux … IH4 IH3 IH2 … HW2l … HV1l … H21) /2 width=1 by fqup_fpbg/ #_ #H
+ <minus_n_O #H0 destruct >(plus_minus_m_m l 1) in HV1l; // -H #HV1l
+ lapply (cpes_cpr_lpr_aux … IH2 IH1 … H21 … HW23 … HV12 … HL12) -H21 /2 width=1 by fqup_fpbg/ #H32