(**************************************************************************)
include "basic_2/relocation/lex_tc.ma".
-include "basic_2/static/lfxs_fsle.ma".
include "basic_2/static/lfeq_fqup.ma".
-include "basic_2/static/lfeq_lfeq.ma".
+include "basic_2/static/lfeq_fsle.ma".
include "basic_2/i_static/tc_lfxs_fqup.ma".
(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***)
(* Note: s_rs_transitive_lex_inv_isid could be invoked in the last auto but makes it too slow *)
lemma tc_lfxs_inv_lex_lfeq: ∀R. c_reflexive … R →
- lfxs_fsle_compatible R →
+ lfxs_fsge_compatible R →
s_rs_transitive … R (λ_.lex R) →
lfeq_transitive R →
∀L1,L2,T. L1 ⪤**[R, T] L2 →