>(yplus_lminus_sn_refl_sn … Hmy2) in ⊢ (%→?); <yplus_assoc #H
lapply (eq_inv_yplus_bi_dx_inj … H) -H
>(yplus_lminus_dx_refl_sn … Hnx1) in ⊢ (%→?); -Hnx1 #H
>(yplus_lminus_sn_refl_sn … Hmy2) in ⊢ (%→?); <yplus_assoc #H
lapply (eq_inv_yplus_bi_dx_inj … H) -H
>(yplus_lminus_dx_refl_sn … Hnx1) in ⊢ (%→?); -Hnx1 #H