1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/notation/constructors/star_0.ma".
16 include "basic_2/notation/constructors/dxbind2_3.ma".
17 include "basic_2/notation/constructors/dxabbr_2.ma".
18 include "basic_2/notation/constructors/dxabst_2.ma".
19 include "basic_2/grammar/term.ma".
21 (* LOCAL ENVIRONMENTS *******************************************************)
23 (* local environments *)
24 inductive lenv: Type[0] ≝
25 | LAtom: lenv (* empty *)
26 | LPair: lenv → bind2 → term → lenv (* binary binding construction *)
29 interpretation "sort (local environment)"
32 interpretation "local environment binding construction (binary)"
33 'DxBind2 L I T = (LPair L I T).
35 interpretation "abbreviation (local environment)"
36 'DxAbbr L T = (LPair L Abbr T).
38 interpretation "abstraction (local environment)"
39 'DxAbst L T = (LPair L Abst T).
41 (* Basic properties *********************************************************)
43 axiom eq_lenv_dec: ∀L1,L2:lenv. Decidable (L1 = L2).
45 (* Basic inversion lemmas ***************************************************)
47 lemma destruct_lpair_lpair: ∀I1,I2,L1,L2,V1,V2. L1.ⓑ{I1}V1 = L2.ⓑ{I2}V2 →
48 ∧∧L1 = L2 & I1 = I2 & V1 = V2.
49 #I1 #I2 #L1 #L2 #V1 #V2 #H destruct /2 width=1/
52 lemma discr_lpair_x_xy: ∀I,V,L. L = L.ⓑ{I}V → ⊥.
56 elim (destruct_lpair_lpair … H) -H #H1 #H2 #H3 destruct /2 width=1/ (**) (* destruct lemma needed *)
60 (* Basic_1: removed theorems 2: chead_ctail c_tail_ind *)