| #a #V2 #W #W2 #T #T2 #HV02 #HW2 #HT2 #H1 #H2 destruct
lapply (cpxs_strap1 … HV10 … HV02) -V0 #HV12
lapply (lsubr_cpx_trans … HT2 (L.ⓓⓝW.V1) ?) -HT2
- /5 width=5 by cpxs_bind, cpxs_flat_dx, cpx_cpxs, lsubr_abst, ex2_3_intro, or3_intro1/
+ /5 width=5 by cpxs_bind, cpxs_flat_dx, cpx_cpxs, lsubr_beta, ex2_3_intro, or3_intro1/
| #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct
/5 width=10 by cpxs_flat_sn, cpxs_bind_dx, cpxs_strap1, ex4_5_intro, or3_intro2/
]