-lemma rex_inv_lex_req: ∀R. c_reflexive … R →
- rex_fsge_compatible R →
- ∀L1,L2,T. L1 ⪤[R,T] L2 →
- ∃∃L. L1 ⪤[R] L & L ≡[T] L2.
+lemma rex_inv_lex_req (R):
+ c_reflexive … R → rex_fsge_compatible R →
+ ∀L1,L2,T. L1 ⪤[R,T] L2 →
+ ∃∃L. L1 ⪤[R] L & L ≡[T] L2.