X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2FBasic_2%2Fsubstitution%2Fgdrop.ma;h=5cef649377b112aa4b87ba9d01415ef9587ee148;hb=0aa60d67f17b528b896e05bbd01038cbc195f69d;hp=47d75a4ea6827cc334ad28df59346b974736ab39;hpb=6ed2537d49a307259db46481469fa44b2cfc56e6;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma
index 47d75a4ea..5cef64937 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/substitution/gdrop.ma
@@ -17,15 +17,15 @@ include "Basic_2/substitution/ldrop.ma".
 (* GLOBAL ENVIRONMENT SLICING ***********************************************)
 
 inductive gdrop (e:nat) (G1:lenv) : predicate lenv ≝
-| gdrop_lt: ∀G2. e < |G1| → ↓[0, |G1| - (e + 1)] G1 ≡ G2 → gdrop e G1 G2
+| gdrop_lt: ∀G2. e < |G1| → ⇓[0, |G1| - (e + 1)] G1 ≡ G2 → 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: ∀G1,G2,e. ↓[e] G1 ≡ G2 → G2 = ⋆ → |G1| ≤ e.
+(*
+fact gdrop_inv_atom2_aux: ∀G1,G2,e. ⇓[e] G1 ≡ G2 → G2 = ⋆ → |G1| ≤ e.
 #G1 #G2 #e * -G2 //
 #G2 #He #HG12 #H destruct
 lapply (ldrop_fwd_O1_length … HG12) -HG12
@@ -33,11 +33,12 @@ lapply (ldrop_fwd_O1_length … HG12) -HG12
 >(commutative_plus e) normalize #H destruct
 qed.
 
-lemma gdrop_inv_atom2: ∀G1,e. ↓[e] G1 ≡ ⋆ → |G1| ≤ e.
+lemma gdrop_inv_atom2: ∀G1,e. ⇓[e] G1 ≡ ⋆ → |G1| ≤ e.
 /2 width=3/ qed-.
 
-lemma gdrop_inv_ge: ∀G1,G2,e. ↓[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆.
+lemma gdrop_inv_ge: ∀G1,G2,e. ⇓[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆.
 #G1 #G2 #e * // #G2 #H1 #_ #H2
 lapply (lt_to_le_to_lt … H1 H2) -H1 -H2 #He
 elim (lt_refl_false … He)
 qed-.
+*)