(* *)
(**************************************************************************)
+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".
(* LOCAL ENVIRONMENTS *******************************************************)
interpretation "sort (local environment)"
'Star = LAtom.
-interpretation "environment construction (binary)"
- 'DxItem2 L I T = (LPair L I T).
-
-interpretation "environment binding construction (binary)"
+interpretation "local environment binding construction (binary)"
'DxBind2 L I T = (LPair L I T).
interpretation "abbreviation (local environment)"
(* Basic properties *********************************************************)
-axiom lenv_eq_dec: ∀L1,L2:lenv. Decidable (L1 = L2).
+axiom eq_lenv_dec: ∀L1,L2:lenv. Decidable (L1 = L2).
(* Basic inversion lemmas ***************************************************)