(* 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/
(* Inversion lemmas with generic extension of a context sensitive relation **)
-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.
#R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL
elim (sex_sdj_split … ceq_ext … HL 𝐈𝐝 ?) -HL
[ #L0 #HL10 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] -H1R