(* *)
(**************************************************************************)
-include "static_2/notation/relations/stareqsn_3.ma".
+include "static_2/notation/relations/approxeqsn_3.ma".
include "static_2/syntax/teqx_ext.ma".
-include "static_2/static/rex.ma".
+include "static_2/static/reqg.ma".
(* SORT-IRRELEVANT EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES ***)
-
+(*
definition reqx: relation3 âĶ â
- rex cdeq.
-
+ reqg sfull.
+*)
interpretation
"sort-irrelevant equivalence on referred entries (local environment)"
- 'StarEqSn T L1 L2 = (reqx T L1 L2).
+ 'ApproxEqSn T L1 L2 = (reqg sfull T L1 L2).
interpretation
"sort-irrelevant ranged equivalence (local environment)"
- 'StarEqSn f L1 L2 = (sex cdeq_ext cfull f L1 L2).
+ 'StarEqSn f L1 L2 = (sex ceqx_ext cfull f L1 L2).
(* Basic properties ***********************************************************)
-
+(*
lemma frees_teqx_conf_reqx:
âf,L1,T1. L1 âĒ ð
+âŠT1âŦ â f â âT2. T1 â T2 â
âL2. L1 â[f] L2 â L2 âĒ ð
+âŠT2âŦ â f.
âI,I1,L1,L2.âT:term. L1.â[I] â[T] L2.â[I1] â
âI2. I â I2 â L1.â[I] â[T] L2.â[I2].
/2 width=2 by rex_bind_repl_dx/ qed-.
-
+*)
+lemma reqg_reqx (S) (T):
+ âL1,L2. L1 â[S,T] L2 â L1 â
[T] L2.
+/2 width=3 by reqg_co/ qed.
+(*
(* Basic inversion lemmas ***************************************************)
lemma reqx_inv_atom_sn:
âI2,L1,K2. âT:term. L1 â[T] K2.â[I2] â
ââI1,K1. L1 = K1.â[I1].
/2 width=5 by rex_fwd_dx/ qed-.
+*)