(* *)
(**************************************************************************)
-include "basic_2/notation/relations/lazyeqsn_3.ma".
-include "basic_2/syntax/lenv_ceq.ma".
+include "basic_2/notation/relations/ideqsn_3.ma".
+include "basic_2/syntax/ceq_ext.ma".
include "basic_2/relocation/lexs.ma".
(* RANGED EQUIVALENCE FOR LOCAL ENVIRONMENTS ********************************)
interpretation
"ranged equivalence (local environment)"
- 'LazyEqSn f L1 L2 = (lreq f L1 L2).
+ 'IdEqSn f L1 L2 = (lreq f L1 L2).
(* Basic properties *********************************************************)