| /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
| /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