include "static_2/syntax/ext2_ext2.ma".
include "static_2/syntax/teqg_teqg.ma".
-include "static_2/static/rex_rex.ma".
include "static_2/static/reqg_length.ma".
(* GENERIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***********)
rex_fsle_compatible (ceqg S).
#S #HS #L1 #L2 #T #HL12
elim (frees_total L1 T) #f #Hf
-/4 width=8 by frees_reqg_conf, rex_fwd_length, lveq_length_eq, sle_refl, ex4_4_intro/
+/4 width=8 by frees_reqg_conf, rex_fwd_length, lveq_length_eq, pr_sle_refl, ex4_4_intro/
qed.
(* Advanced properties ******************************************************)