-(* Basic_2A1: includes: lpx_sn_trans *)
-theorem lexs_trans (RN) (RP) (f): lexs_transitive RN RN RN RP →
- lexs_transitive RP RP RN RP →
- Transitive … (lexs RN RP f).
-#RN #RP #f #HN #HP #L1 #L0 #H elim H -L1 -L0 -f
+theorem lexs_trans_gen (RN1) (RP1) (RN2) (RP2) (RN) (RP) (f):
+ lexs_transitive RN1 RN2 RN RN1 RP1 →
+ lexs_transitive RP1 RP2 RP RN1 RP1 →
+ ∀L1,L0. L1 ⦻*[RN1, RP1, f] L0 →
+ ∀L2. L0 ⦻*[RN2, RP2, f] L2 →
+ L1 ⦻*[RN, RP, f] L2.
+#RN1 #RP1 #RN2 #RP2 #RN #RP #f #HN #HP #L1 #L0 #H elim H -L1 -L0 -f