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/substitution/gdrop.ma".
17 (* GLOBAL ENVIRONMENT SLICING ***********************************************)
19 (* Main properties **********************************************************)
21 theorem gdrop_mono: ∀G,G1,e. ⇩[e] G ≡ G1 → ∀G2. ⇩[e] G ≡ G2 → G1 = G2.
22 #G #G1 #e #H elim H -G -G1
24 >(gdrop_inv_gt … H He) -H -He //
26 >(gdrop_inv_eq … H He) -H -He //
27 | #I #G #G1 #V #He #_ #IHG1 #G2 #H
28 lapply (gdrop_inv_lt … H He) -H -He /2 width=1/
32 lemma gdrop_dec: ∀G1,G2,e. Decidable (⇩[e] G1 ≡ G2).
34 elim (gdrop_total e G1) #G #HG1
35 elim (genv_eq_dec G G2) #HG2
36 [ destruct /2 width=1/
38 lapply (gdrop_mono … HG1 … HG12) -HG1 -HG12 /2 width=1/