- support for candidates of reducibility continues ...

[helm.git] / matita / matita / contribs / lambda_delta / Basic_2 / substitution / gdrop.ma

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 47d75a4ea6827cc334ad28df59346b974736ab39..5cef649377b112aa4b87ba9d01415ef9587ee148 100644 (file)
--- 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: â\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
@@ -33,11 +33,12 @@ 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-.
+*)