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