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 ***********)
lemma frees_reqg_conf (S):
reflexive … S →
- â\88\80f,L1,T. L1 â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f →
- â\88\80L2. L1 â\89\9b[S,T] L2 â\86\92 L2 â\8a¢ ð\9d\90\85+â\9dªTâ\9d« ≘ f.
+ â\88\80f,L1,T. L1 â\8a¢ ð\9d\90\85+â\9d¨Tâ\9d© ≘ f →
+ â\88\80L2. L1 â\89\9b[S,T] L2 â\86\92 L2 â\8a¢ ð\9d\90\85+â\9d¨Tâ\9d© ≘ f.
/3 width=7 by frees_seqg_conf, rex_inv_frees/ qed-.
(* Properties with free variables inclusion for restricted closures *******)
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 ******************************************************)