lapply (scpes_inv_lstas_eq … HVV1 … HVX … HVX1) -HVV1 -HVX #HXX1
lapply (cpcs_canc_sn … HXX1 … HXW) -X
elim (lift_total X1 0 (i+1))
lapply (drop_fwd_drop2 … HLK1)
/4 width=12 by cpcs_lift, lstas_cast, lstas_ldef, ex2_intro/
]
lapply (scpes_inv_lstas_eq … HVV1 … HVX … HVX1) -HVV1 -HVX #HXX1
lapply (cpcs_canc_sn … HXX1 … HXW) -X
elim (lift_total X1 0 (i+1))
lapply (drop_fwd_drop2 … HLK1)
/4 width=12 by cpcs_lift, lstas_cast, lstas_ldef, ex2_intro/
]