-lemma rexs_inv_lex_req: ∀R. c_reflexive … R →
- rex_fsge_compatible R →
- s_rs_transitive … R (λ_.lex R) →
- req_transitive R →
- ∀L1,L2,T. L1 ⪤*[R,T] L2 →
- ∃∃L. L1 ⪤[CTC … R] L & L ≡[T] L2.
+lemma rexs_inv_lex_req (R):
+ c_reflexive … R → rex_fsge_compatible R →
+ s_rs_transitive … R (λ_.lex R) → R_transitive_req R →
+ ∀L1,L2,T. L1 ⪤*[R,T] L2 →
+ ∃∃L. L1 ⪤[CTC … R] L & L ≡[T] L2.