- elim (scpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW130 #_ #H destruct -T30 -l0
- elim (snv_fwd_da … HV1) #l #HV1l
- elim (snv_fwd_da … HW10) #l0 #HW10l
- lapply (cprs_scpds_div … HW130 … HW10l … 1 HVW1) -W30 #HVW10
- elim (da_scpes_aux … IH4 IH1 IH2 … HW10l … HV1l … HVW10) /2 width=1 by fqup_fpbg/
- #_ #Hl <minus_n_O #H destruct >(plus_minus_m_m l 1) in HV1l; // -Hl #HV1l
+ elim (scpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW130 #_ #H destruct -T30 -d0
+ elim (snv_fwd_da … HV1) #d #HV1d
+ elim (snv_fwd_da … HW10) #d0 #HW10d
+ lapply (cprs_scpds_div … HW130 … HW10d … 1 HVW1) -W30 #HVW10
+ elim (da_scpes_aux … IH4 IH1 IH2 … HW10d … HV1d … HVW10) /2 width=1 by fqup_fpbg/
+ #_ #Hd <minus_n_O #H destruct >(plus_minus_m_m d 1) in HV1d; // -Hd #HV1d