+definition lpx_sn_confluent: relation6 (relation3 lenv term term)
+ (relation3 lenv term term) … ≝
+ λR1,R2,RN1,RP1,RN2,RP2.
+ ∀f,L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 →
+ ∀L1. L0 ⦻*[RN1, RP1, f] L1 → ∀L2. L0 ⦻*[RN2, RP2, f] L2 →
+ ∃∃T. R2 L1 T1 T & R1 L2 T2 T.
+
+definition lexs_transitive: relation4 (relation3 lenv term term)
+ (relation3 lenv term term) … ≝
+ λR1,R2,RN,RP.
+ ∀f,L1,T1,T. R1 L1 T1 T → ∀L2. L1 ⦻*[RN, RP, f] L2 →
+ ∀T2. R2 L2 T T2 → R1 L1 T1 T2.
+