- lapply (IH1 … HV1 … HV12 … HL12) [ /2 width=1/ ] #HV2
- lapply (IH1 … HT1 … HT12 … HL12) [ /2 width=1/ ] #HT2
- elim (IH3 … HVW1 … HV12 … HL12) -HVW1 -HV12 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12
- elim (dxprs_cprs_lpr_aux … IH2 IH1 IH3 … HTU1 … T2 … HL12) // [2,3: /2 width=1/ ] -IH2 -IH1 -IH3 -HT1 -HT12 -HTU1 #X #HTU2 #H
- elim (cprs_fwd_abst1 … H Abst W1) -H #W20 #U2 #HW120 #_ #H destruct
- lapply (cprs_lpr_conf … HL12 … HW10) -L1 #HW10
- lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120
- lapply (cpcs_canc_sn … HW12 HW120) -W10 #HW20
- elim (cpcs_inv_cprs … HW20) -HW20 #W0 #HW20 #HW200
- lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?) [ /2 width=1/ ] -HW200 -HTU2 /2 width=8/
- | #b #V2 #W20 #T20 #T2 #HV12 #HT202 #H1 #H2 destruct
- elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20
- elim (dxprs_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30
- lapply (cprs_div … HW10 … HW230) -W30 #HW120
- lapply (cpcs_lpr_conf … HL12 … HW120) -HW120 #HW120
- elim (IH3 … HVW1 … HV12 … HL12) // [2: /2 width=1/ ] -HVW1 #W2 #HVW2 #HW102
- lapply (cpcs_canc_sn … HW102 … HW120) -W10 #HW220
- lapply (IH1 … HV12 … HL12) // [ /2 width=1/ ] #HV2 -HV1
- lapply (IH1 … HW20 … W20 … HL12) // [ /2 width=1/ ] -HW20 #HW20
- lapply (IH1 … HT20 … HT202 … (L2.ⓛW20) ?) [1,2: /2 width=1/ ] -HT20 #HT2
- lapply (IH2 … HVW2) //
- [ @(ygt_yprs_trans … L1 L1 … V1) (**) (* auto /4 width=5/ is a bit slow even with trace *)
- [ /2 width=1 by fsupp_ygt/
- | /3 width=1 by cprs_lpr_yprs, cpr_cprs/
- ]
- ] #HW2
- elim (snv_fwd_ssta … HW20) #l0 #U20 #HWU20
- elim (ssta_fwd_correct … HVW2) <minus_plus_m_m #U2 #HWU2
- elim (ssta_cpcs_lpr_aux … IH1 IH3 … HWU2 … HWU20 … HW220 … L2) // -IH3
- [2: /4 width=4 by ygt_yprs_trans, fsupp_ygt, ypr_yprs, ypr_lpr/
- |3: @(ygt_yprs_trans … L1 L2 … V2) (**) (* auto not tried *)
- [ @(ygt_yprs_trans … L1 L1 … V1)
- [ /2 width=1 by fsupp_ygt/
- | /3 width=1 by cprs_lpr_yprs, cpr_cprs/
- ]
- | /3 width=2 by ypr_ssta, ypr_yprs/
- ]
- ] #H #_ destruct -IH2 -U2
- lapply (IH4 … HT2 (L2.ⓓV2) ?)
- [ /2 width=6/
- | @(ygt_yprs_trans … (L1.ⓛW20) … T2) (**) (* auto /5 width=5/ is too slow even with trace timeout=35 *)
- [ /4 width=4 by ygt_yprs_trans, fsupp_ygt, ypr_yprs, ypr_cpr/
- | /4 width=1 by ypr_yprs, ypr_lpr, lpr_pair/
- ]
- ] -L1 -V1 -W2 -T20 -U20 -W20 -l0 /2 width=1/
+ lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
+ lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
+ elim (scpds_cpr_lpr_aux … IH2 IH3 … HVW1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW1 -HV12 #XV #HVW2 #HXV
+ elim (scpds_cpr_lpr_aux … IH2 IH3 … HTU1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ -HTU1 -HT12 #X #HTU2 #H
+ elim (cprs_inv_abst1 … H) -H #XW #U2 #HXW #_ #H destruct -IH1 -IH3 -IH2 -L1
+ elim (cprs_conf … HXV … HXW) -W1 #W2 #HXV #HXW
+ lapply (scpds_cprs_trans … HVW2 … HXV) -XV
+ lapply (scpds_cprs_trans … (ⓛ{a}W2.U2) … HTU2 ?)
+ /2 width=7 by snv_appl, cprs_bind/
+ | #b #V2 #W10 #W20 #T10 #T20 #HV12 #HW120 #HT120 #H1 #H2 destruct
+ elim (snv_inv_bind … HT1) -HT1 #HW10 #HT10
+ 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_k_k d 1) in HV1d; // -Hd #HV1d
+ lapply (scpes_cpr_lpr_aux … IH2 IH3 … HVW10 … HW120 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW10 #HVW20
+ lapply (IH2 … HV1d … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1d #HV2d
+ lapply (IH2 … HW10d … HW120 … HL12) /2 width=1 by fqup_fpbg/ -HW10d #HW20d
+ lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
+ lapply (IH1 … HW120 … HL12) /2 width=1 by fqup_fpbg/ -HW10 #HW20
+ lapply (IH1 … HT10 … HT120 … (L2.ⓛW20) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT10 #HT20
+ @snv_bind /2 width=1 by snv_cast_scpes/
+ @(lsubsv_snv_trans … HT20) -HT20
+ @(lsubsv_beta … (d-1)) //
+ @shnv_cast [1,2: // ] #d0 #Hd0
+ lapply (scpes_le_aux … IH4 IH1 IH2 IH3 … HW20d … HV2d … d0 … HVW20) -IH4 -IH3 -IH2 -IH1 -HW20d -HV2d -HVW20
+ /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/