(* GLOBAL ENVIRONMENT SLICING ***********************************************)
inductive gdrop (e:nat) (G1:lenv) : predicate lenv ≝
-| gdrop_lt: â\88\80G2. e < |G1| â\86\92 â\86\93[0, |G1| - (e + 1)] G1 â\89¡ G2 â\86\92 gdrop e G1 G2
+| gdrop_lt: â\88\80G2. e < |G1| â\86\92 â\87\93[0, |G1| - (e + 1)] G1 â\89¡ G2 â\86\92 gdrop e G1 G2
| gdrop_ge: |G1| ≤ e → gdrop e G1 (⋆)
.
-interpretation "global slicing" 'RDrop e G1 G2 = (gdrop e G1 G2).
+interpretation "global slicing" 'RGDrop e G1 G2 = (gdrop e G1 G2).
(* basic inversion lemmas ***************************************************)
-
-fact gdrop_inv_atom2_aux: â\88\80G1,G2,e. â\86\93[e] G1 â\89¡ G2 â\86\92 G2 = â\8b\86 â\86\92 |G1| â\89¤ e.
+(*
+fact gdrop_inv_atom2_aux: â\88\80G1,G2,e. â\87\93[e] G1 â\89¡ G2 â\86\92 G2 = â\8b\86 â\86\92 |G1| â\89¤ e.
#G1 #G2 #e * -G2 //
#G2 #He #HG12 #H destruct
lapply (ldrop_fwd_O1_length … HG12) -HG12
>(commutative_plus e) normalize #H destruct
qed.
-lemma gdrop_inv_atom2: â\88\80G1,e. â\86\93[e] G1 â\89¡ â\8b\86 â\86\92 |G1| â\89¤ e.
+lemma gdrop_inv_atom2: â\88\80G1,e. â\87\93[e] G1 â\89¡ â\8b\86 â\86\92 |G1| â\89¤ e.
/2 width=3/ qed-.
-lemma gdrop_inv_ge: â\88\80G1,G2,e. â\86\93[e] G1 â\89¡ G2 â\86\92 |G1| â\89¤ e â\86\92 G2 = â\8b\86.
+lemma gdrop_inv_ge: â\88\80G1,G2,e. â\87\93[e] G1 â\89¡ G2 â\86\92 |G1| â\89¤ e â\86\92 G2 = â\8b\86.
#G1 #G2 #e * // #G2 #H1 #_ #H2
lapply (lt_to_le_to_lt … H1 H2) -H1 -H2 #He
elim (lt_refl_false … He)
qed-.
+*)