(* *)
(**************************************************************************)
-include "static_2/notation/relations/stareq_3.ma".
-include "static_2/syntax/cext2.ma".
+(*
+include "static_2/notation/relations/approxeq_3.ma".
+*)
+include "static_2/syntax/teqg_ext.ma".
include "static_2/syntax/teqx.ma".
(* EXTENDED SORT-IRRELEVANT EQUIVALENCE *************************************)
-
+(*
definition teqx_ext: relation bind ≝
- ext2 teqx.
-
-definition cdeq: relation3 lenv term term ≝
- λL. teqx.
-
-definition cdeq_ext: relation3 lenv bind bind ≝
- cext2 cdeq.
-
+ teqg_ext sfull.
+
+definition ceqx: relation3 lenv term term ≝
+ ceqg sfull.
+*)
+definition ceqx_ext: relation3 lenv bind bind ≝
+ ceqg_ext sfull.
+(*
interpretation
- "context-free sort-irrelevant equivalence (binder)"
- 'StarEq I1 I2 = (teqx_ext I1 I2).
+ "context-free sort-irrelevant equivalence (binder)"
+ 'StarEq I1 I2 = (teqx_ext I1 I2).
interpretation
- "context-dependent sort-irrelevant equivalence (term)"
- 'StarEq L T1 T2 = (cdeq L T1 T2).
+ "context-dependent sort-irrelevant equivalence (term)"
+ 'StarEq L T1 T2 = (cdeq L T1 T2).
interpretation
- "context-dependent sort-irrelevant equivalence (binder)"
- 'StarEq L I1 I2 = (cdeq_ext L I1 I2).
+ "context-dependent sort-irrelevant equivalence (binder)"
+ 'ApproxEq L I1 I2 = (cdeq_ext L I1 I2).
+*)