- | #b #V2 #W20 #W2 #T20 #T2 #HV12 #HW202 #HT202 #H1 #H2 destruct
- elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20
- elim (cpds_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30
- lapply (cprs_div … HW10 … HW230) -W30 #HW120
- lapply (snv_ssta_aux … IH4 … Hl0 … HVW1) /2 width=1 by fsupp_ygt/ #HW10
- lapply (ssta_da_conf … HVW1 … Hl0) <minus_plus_m_m #HlW10
- elim (snv_fwd_da … HW20) #l #Hl
- lapply (da_cpcs_aux … IH1 IH2 … HlW10 … Hl … HW120) // -HlW10
- /3 width=5 by ygt_fpbs_trans, fsupp_ygt, ssta_fpbs/ #H destruct
- lapply (IH2 … Hl0 … HV12 … HL12) /2 width=1 by fsupp_ygt/ #HlV2
- lapply (IH2 … Hl … HW202 … HL12) /2 width=1 by fsupp_ygt/ #HlW2
- elim (ssta_cpr_lpr_aux … IH3 … Hl0 … HVW1 … HV12 … HL12) /2 width=1 by fsupp_ygt/ #W3 #HV2W3 #HW103
- lapply (ssta_da_conf … HV2W3 … HlV2) <minus_plus_m_m #HlW3
- lapply (cpcs_cpr_strap1 … HW120 … HW202) -HW120 #HW102
- lapply (lpr_cpcs_conf … HL12 … HW102) -HW102 #HW102
- lapply (cpcs_canc_sn … HW103 … HW102) -W10 #HW32
- lapply (IH1 … HV12 … HL12) /2 width=1 by fsupp_ygt/ -HV1 #HV2
- lapply (IH1 … HW202 … HL12) /2 width=1 by fsupp_ygt/ -HW20 #HW2
- lapply (IH1 … HT20 … HT202 … (L2.ⓛW2) ?) /2 width=1 by fsupp_ygt, lpr_pair/ -HT20 #HT2
- lapply (snv_ssta_aux … IH4 … HlV2 … HV2W3)
- /3 width=5 by ygt_fpbs_trans, fsupp_ygt, cpr_lpr_fpbs/ #HW3
- lapply (lsubsv_snv_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /3 width=3 by snv_bind, snv_cast/
- @(lsubsv_abbr … l) /3 width=7 by fsupp_ygt/ #W #W0 #l0 #Hl0 #HV2W #HW20
- lapply (lsstas_ssta_conf_pos … HV2W3 … HV2W) -HV2W #HW3W
- @(lsstas_cpcs_lpr_aux … IH1 IH2 IH3 … HlW3 … HW3W … HlW2 … HW20 … HW32) //
- [ /3 width=9 by ygt_fpbs_trans, fsupp_ygt, cpr_lpr_ssta_fpbs/
- | /3 width=5 by ygt_fpbs_trans, fsupp_ygt, cpr_lpr_fpbs/
- ]
+ | #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 -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
+ lapply (scpes_cpr_lpr_aux … IH2 IH3 … HVW10 … HW120 … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HVW10 #HVW20
+ lapply (IH2 … HV1l … HV12 … HL12) /2 width=1 by fqup_fpbg/ -HV1l #HV2l
+ lapply (IH2 … HW10l … HW120 … HL12) /2 width=1 by fqup_fpbg/ -HW10l #HW20l
+ 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 … (l-1)) //
+ @shnv_cast [1,2: // ] #l0 #Hl0
+ lapply (scpes_le_aux … IH4 IH1 IH2 IH3 … HW20l … HV2l … l0 … HVW20) -IH4 -IH3 -IH2 -IH1 -HW20l -HV2l -HVW20
+ /3 width=5 by fpbg_fpbs_trans, fqup_fpbg, cpr_lpr_fpbs, le_S_S/