(* *)
(**************************************************************************)
+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)"
interpretation "abstraction (local environment)"
'DxAbst L T = (LPair L Abst T).
+(* Basic properties *********************************************************)
+
+axiom eq_lenv_dec: ∀L1,L2:lenv. Decidable (L1 = L2).
+
(* Basic inversion lemmas ***************************************************)
lemma destruct_lpair_lpair: ∀I1,I2,L1,L2,V1,V2. L1.ⓑ{I1}V1 = L2.ⓑ{I2}V2 →