+lemma rex_inv_req_lex (R):
+ c_reflexive … R → f_confluent1_next R ceq →
+ ∀L1,L2,T. L1 ⪤[R,T] L2 →
+ ∃∃L. L1 ≡[T] L & L ⪤[R] L2.
+#R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL
+elim (sex_sdj_split_dx … ceq_ext … HL 𝐢) -HL
+[ #L0 #HL10 #HL02
+ lapply (sex_sdj … HL02 f1 ?) /2 width=1 by pr_sdj_isi_sn/ #H
+ /3 width=5 by (* 2x *) ex2_intro/
+|*: /2 width=1 by ext2_refl, pr_sdj_isi_dx/
+ #g #I #K #n #HLK #Hg @H2R /width=7 by/ (**) (* no auto with H2R *)
+]
+qed-.
+
+(* Forward lemmas with generic extension of a context sensitive relation **)
+
+lemma rex_fwd_lex_req (R):