(* Properties with generic extension of a context-sensitive relation ********)
-lemma rex_lex: ∀R,L1,L2. L1 ⪤[R] L2 → ∀T. L1 ⪤[R, T] L2.
+lemma rex_lex: ∀R,L1,L2. L1 ⪤[R] L2 → ∀T. L1 ⪤[R,T] L2.
#R #L1 #L2 * #f #Hf #HL12 #T
elim (frees_total L1 T) #g #Hg
/4 width=5 by sex_sdj, sdj_isid_sn, ex2_intro/
lemma rex_inv_lex_req: ∀R. c_reflexive … R →
rex_fsge_compatible R →
- ∀L1,L2,T. L1 ⪤[R, T] L2 →
+ ∀L1,L2,T. L1 ⪤[R,T] L2 →
∃∃L. L1 ⪤[R] L & L ≡[T] L2.
#R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL
elim (sex_sdj_split … ceq_ext … HL 𝐈𝐝 ?) -HL