- (∀g,I,K,V,n. ⬇*[n] L ≡ K.ⓑ{I}V → ⫱*[n] f = ⫯g → lexs_pw_confluent2_R RN1 RN2 RN1 RP1 RN2 RP2 g K V) →
- (∀g,I,K,V,n. ⬇*[n] L ≡ K.ⓑ{I}V → ⫱*[n] f = ↑g → lexs_pw_confluent2_R RP1 RP2 RN1 RP1 RN2 RP2 g K V) →
+ (∀g,I,K,V,n. ⬇*[n] L ≡ K.ⓑ{I}V → ⫯g = ⫱*[n] f → lexs_pw_confluent2_R RN1 RN2 RN1 RP1 RN2 RP2 g K V) →
+ (∀g,I,K,V,n. ⬇*[n] L ≡ K.ⓑ{I}V → ↑g = ⫱*[n] f → lexs_pw_confluent2_R RP1 RP2 RN1 RP1 RN2 RP2 g K V) →