-fact lexs_inv_next1_aux: â\88\80RN,RP,f,X,Y. X ⦻*[RN, RP, f] Y → ∀g,J,K1,W1. X = K1.ⓑ{J}W1 → f = ⫯g →
- â\88\83â\88\83K2,W2. K1 ⦻*[RN, RP, g] K2 & RN K1 W1 W2 & Y = K2.ⓑ{J}W2.
+fact lexs_inv_next1_aux: â\88\80RN,RP,f,X,Y. X ⪤*[RN, RP, f] Y → ∀g,J,K1,W1. X = K1.ⓑ{J}W1 → f = ⫯g →
+ â\88\83â\88\83K2,W2. K1 ⪤*[RN, RP, g] K2 & RN K1 W1 W2 & Y = K2.ⓑ{J}W2.