- elim (cpds_inv_abst1 … HT10) -HT10 #W3 #U3 #HW3 #_ #H destruct -U3
- lapply (cprs_div … HW3 … HW10) -W3 #HWW1
- lapply (da_sta_conf … HVW1 … Hl0) <minus_plus_m_m #H
- elim (snv_fwd_da … HW) #l1 #Hl1
- lapply (IH3 … HV1 … 1 … Hl0 W1 ?) /2 width=2 by fqup_fpbg, sta_lstas/ #HW1
- lapply (da_cpcs_aux … IH2 IH1 … Hl1 … H … HWW1) -H
- /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, sta_fpbs/ #H destruct
- lapply (IH1 … HV1 … Hl0 … HV12 … HL12) -HV1 -Hl0 -HV12 [ /2 by fqup_fpbg/ ] #Hl0
- lapply (IH1 … Hl1 … HW2 … HL12) -Hl1 // /2 width=1 by fqup_fpbg/ -HW
- lapply (IH1 … HU1 … Hl … HU12 (L2.ⓛW2) ?) -IH1 -HU1 -Hl -HU12 [1,2: /2 by fqup_fpbg, lpr_pair/ ] -HL12 -HW2
+ elim (cpds_inv_abst1 … HTU1) -HTU1 #W3 #U3 #HW3 #_ #H destruct -U3 -l1
+ elim (snv_fwd_da … HV1) #l1 #Hl1
+ elim (snv_fwd_da … HW) #l0 #Hl0
+ lapply (cpds_div … W … 0 … HVW1) /2 width=2 by cprs_cpds/ -W3 #H
+ elim (da_cpes_aux … IH3 IH2 IH1 … Hl0 … Hl1 … H) -IH3 -IH2 -H /2 width=1 by fqup_fpbg/ #_ #H1
+ <minus_n_O #H destruct >(plus_minus_m_m l1 1) in Hl1; // -H1 #Hl1
+ lapply (IH1 … HV1 … Hl1 … HV12 … HL12) -HV1 -Hl1 -HV12 [ /2 by fqup_fpbg/ ]
+ lapply (IH1 … Hl0 … HW2 … HL12) -Hl0 /2 width=1 by fqup_fpbg/ -HW
+ lapply (IH1 … HU … Hl … HU2 (L2.ⓛW2) ?) -IH1 -HU -Hl -HU2 [1,2: /2 by fqup_fpbg, lpr_pair/ ] -HL12 -HW2