- lapply (cpcs_ext_bind … HV12 … HU20 b Abbr) -HV12 -HU20 #HU20
- lapply (cpcs_canc_sn … HW12 HW1W) -W1 #HW2
- elim (lsubss_ssta_trans … HTU20 (L2.ⓓV2) ?) -HTU20
- [ #U #HTU20 #HUU20 -HWV0 -W2
- lapply (cpcs_bind1 b … V2 V2 … HUU20) // -HUU20 #HUU20
- lapply (cpcs_canc_dx … HU20 … HUU20) -U20 #HU2
- lapply (cpcs_cpr_strap2 … (ⓐV1.ⓛ{b}W.U2) … HU2) [ /2 width=1/ ] /3 width=3/
- | -b -l -V -V1 -T2 -T20 -U0 -U2 -U20 /2 width=6/
+ lapply (cpcs_canc_sn … HW12 HW112) -W1 #HW12
+ lapply (cpcs_canc_sn … HW12 HW20) -HW12 #HW12
+ elim (lsubsv_ssta_trans … HTU20 (L2.ⓓⓝW20.V2)) -HTU20
+ [ #U #HTU20 #HUU20 -HVW12 -HWV20 -HW12
+ @(ex2_intro … (ⓓ{b}ⓝW20.V2.U)) [ /3 width=1/ ] -HTU20
+ @(cpcs_canc_dx … (ⓓ{b}ⓝW20.V2.U20)) [2: /2 width=1/ ] -HUU20
+ @(cpcs_cpr_strap1 … (ⓐV2.ⓛ{b}W20.U20)) [2: /2 width=1/ ]
+ /3 by cpcs_bind2, cpcs_flat/
+ | -HU20 -HW20 -HV12 /3 width=5 by lsubsv_abbr, snv_cast/