X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fgget.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fsubstitution%2Fgget.ma;h=eb5c8fdabc78625e42fe64a2787c6b5f620fa66a;hb=c60524dec7ace912c416a90d6b926bee8553250b;hp=acf9602be26d724d701b468fa78cc029837b0b49;hpb=f10cfe417b6b8ec1c7ac85c6ecf5fb1b3fdf37db;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/gget.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/gget.ma
index acf9602be..eb5c8fdab 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/gget.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/gget.ma
@@ -17,19 +17,19 @@ include "basic_2/grammar/genv.ma".
 
 (* GLOBAL ENVIRONMENT READING ***********************************************)
 
-inductive gget (e:nat): relation genv ≝
-| gget_gt: ∀G. |G| ≤ e → gget e G (⋆)
-| gget_eq: ∀G. |G| = e + 1 → gget e G G
-| gget_lt: ∀I,G1,G2,V. e < |G1| → gget e G1 G2 → gget e (G1. ⓑ{I} V) G2
+inductive gget (m:nat): relation genv ≝
+| gget_gt: ∀G. |G| ≤ m → gget m G (⋆)
+| gget_eq: ∀G. |G| = m + 1 → gget m G G
+| gget_lt: ∀I,G1,G2,V. m < |G1| → gget m G1 G2 → gget m (G1. ⓑ{I} V) G2
 .
 
 interpretation "global reading"
-   'RDrop e G1 G2 = (gget e G1 G2).
+   'RDrop m G1 G2 = (gget m G1 G2).
 
 (* basic inversion lemmas ***************************************************)
 
-lemma gget_inv_gt: ∀G1,G2,e. ⬇[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆.
-#G1 #G2 #e * -G1 -G2 //
+lemma gget_inv_gt: ∀G1,G2,m. ⬇[m] G1 ≡ G2 → |G1| ≤ m → G2 = ⋆.
+#G1 #G2 #m * -G1 -G2 //
 [ #G #H >H -H >commutative_plus #H (**) (* lemma needed here *)
   lapply (le_plus_to_le_r … 0 H) -H #H
   lapply (le_n_O_to_eq … H) -H #H destruct
@@ -40,8 +40,8 @@ lemma gget_inv_gt: ∀G1,G2,e. ⬇[e] G1 ≡ G2 → |G1| ≤ e → G2 = ⋆.
 ]
 qed-.
 
-lemma gget_inv_eq: ∀G1,G2,e. ⬇[e] G1 ≡ G2 → |G1| = e + 1 → G1 = G2.
-#G1 #G2 #e * -G1 -G2 //
+lemma gget_inv_eq: ∀G1,G2,m. ⬇[m] G1 ≡ G2 → |G1| = m + 1 → G1 = G2.
+#G1 #G2 #m * -G1 -G2 //
 [ #G #H1 #H2 >H2 in H1; -H2 >commutative_plus #H (**) (* lemma needed here *)
   lapply (le_plus_to_le_r … 0 H) -H #H
   lapply (le_n_O_to_eq … H) -H #H destruct
@@ -51,9 +51,9 @@ lemma gget_inv_eq: ∀G1,G2,e. ⬇[e] G1 ≡ G2 → |G1| = e + 1 → G1 = G2.
 ]
 qed-.
 
-fact gget_inv_lt_aux: ∀I,G,G1,G2,V,e. ⬇[e] G ≡ G2 → G = G1. ⓑ{I} V →
-                      e < |G1| → ⬇[e] G1 ≡ G2.
-#I #G #G1 #G2 #V #e * -G -G2
+fact gget_inv_lt_aux: ∀I,G,G1,G2,V,m. ⬇[m] G ≡ G2 → G = G1. ⓑ{I} V →
+                      m < |G1| → ⬇[m] G1 ≡ G2.
+#I #G #G1 #G2 #V #m * -G -G2
 [ #G #H1 #H destruct #H2
   lapply (le_to_lt_to_lt … H1 H2) -H1 -H2 normalize in ⊢ (? % ? → ?); >commutative_plus #H
   lapply (lt_plus_to_lt_l … 0 H) -H #H
@@ -64,18 +64,18 @@ fact gget_inv_lt_aux: ∀I,G,G1,G2,V,e. ⬇[e] G ≡ G2 → G = G1. ⓑ{I} V →
 ]
 qed-.
 
-lemma gget_inv_lt: ∀I,G1,G2,V,e.
-                    ⬇[e] G1. ⓑ{I} V ≡ G2 → e < |G1| → ⬇[e] G1 ≡ G2.
+lemma gget_inv_lt: ∀I,G1,G2,V,m.
+                    ⬇[m] G1. ⓑ{I} V ≡ G2 → m < |G1| → ⬇[m] G1 ≡ G2.
 /2 width=5 by gget_inv_lt_aux/ qed-.
 
 (* Basic properties *********************************************************)
 
-lemma gget_total: ∀e,G1. ∃G2. ⬇[e] G1 ≡ G2.
-#e #G1 elim G1 -G1 /3 width=2/
+lemma gget_total: ∀m,G1. ∃G2. ⬇[m] G1 ≡ G2.
+#m #G1 elim G1 -G1 /3 width=2 by gget_gt, ex_intro/
 #I #V #G1 * #G2 #HG12
-elim (lt_or_eq_or_gt e (|G1|)) #He
+elim (lt_or_eq_or_gt m (|G1|)) #Hm
 [ /3 width=2/
-| destruct /3 width=2/
-| @ex_intro [2: @gget_gt normalize /2 width=1/ | skip ] (**) (* explicit constructor *)
+| destruct /3 width=2 by gget_eq, ex_intro/
+| @ex_intro [2: @gget_gt normalize /2 width=1 by/ | skip ] (**) (* explicit constructor *)
 ]
 qed-.