(* *)
(**************************************************************************)
-include "ground_2/list.ma".
+include "ground_2/lib/list.ma".
+include "basic_2/notation/constructors/star_0.ma".
+include "basic_2/notation/constructors/dxbind2_3.ma".
+include "basic_2/notation/constructors/dxabbr_2.ma".
+include "basic_2/notation/constructors/dxabst_2.ma".
include "basic_2/grammar/term.ma".
(* GLOBAL ENVIRONMENTS ******************************************************)
interpretation "sort (global environment)"
'Star = (nil2 bind2 term).
-interpretation "environment construction (binary)"
- 'DxItem2 L I T = (cons2 bind2 term I T L).
-
-interpretation "environment binding construction (binary)"
+interpretation "global environment binding construction (binary)"
'DxBind2 L I T = (cons2 bind2 term I T L).
interpretation "abbreviation (global environment)"
(* Basic properties *********************************************************)
-axiom genv_eq_dec: ∀T1,T2:genv. Decidable (T1 = T2).
+axiom eq_genv_dec: ∀G1,G2:genv. Decidable (G1 = G2).