X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Fsubstitution%2Flsubs_sfr.ma;h=b71f25e5138b4877d49073a52009ebe56f38736f;hb=5ea90cbbb01fe0bf3b77221d9e6c87002982621f;hp=fb71a175c4b3d73d7c4af780e5f83b324f9039ad;hpb=78d4844bcccb3deb58a3179151c3045298782b18;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma
index fb71a175c..b71f25e51 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/lsubs_sfr.ma
@@ -16,53 +16,58 @@ include "basic_2/substitution/lsubs.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
 
-(* top element of the refinement *)
+(* bottom element of the refinement *)
 definition sfr: nat → nat → predicate lenv ≝
-   λd,e. NF … (lsubs d e) (lsubs d e …).
+   λd,e. NF_sn … (lsubs d e) (lsubs d e …).
 
 interpretation
    "local environment full refinement (substitution)"
-   'SubEqTop d e L = (sfr d e L).
+   'SubEqBottom d e L = (sfr d e L).
 
 (* Basic properties *********************************************************)
 
-lemma sfr_atom: ∀d,e. ≼ [d, e] ⋆.
+lemma sfr_atom: ∀d,e. ≽ [d, e] ⋆.
 #d #e #L #H
-elim (lsubs_inv_atom1 … H) -H
+elim (lsubs_inv_atom2 … H) -H
 [ #H destruct //
 | * #H1 #H2 destruct //
 ]
 qed.
 
-lemma sfr_OO: ∀L. ≼ [0, 0] L.
+lemma sfr_OO: ∀L. ≽ [0, 0] L.
 // qed.
 
-lemma sfr_abbr: ∀L,V,e. ≼ [0, e] L → ≼ [0, e + 1] L.ⓓV.
+lemma sfr_abbr: ∀L,V,e. ≽ [0, e] L → ≽ [0, e + 1] L.ⓓV.
 #L #V #e #HL #K #H
-elim (lsubs_inv_abbr1 … H ?) -H // <minus_plus_m_m #X #HLX #H destruct
+elim (lsubs_inv_abbr2 … H ?) -H // <minus_plus_m_m #X #HLX #H destruct
 lapply (HL … HLX) -HL -HLX /2 width=1/
 qed.
 
-lemma sfr_skip: ∀I,L,V,d,e. ≼ [d, e] L → ≼ [d + 1, e] L.ⓑ{I}V.
+lemma sfr_abbr_O: ∀L,V. ≽[0,1] L.ⓓV.
+#L #V
+@(sfr_abbr … 0) //
+qed.
+
+lemma sfr_skip: ∀I,L,V,d,e. ≽ [d, e] L → ≽ [d + 1, e] L.ⓑ{I}V.
 #I #L #V #d #e #HL #K #H
-elim (lsubs_inv_skip1 … H ?) -H // <minus_plus_m_m #J #X #W #HLX #H destruct
+elim (lsubs_inv_skip2 … H ?) -H // <minus_plus_m_m #J #X #W #HLX #H destruct
 lapply (HL … HLX) -HL -HLX /2 width=1/
 qed.
 
 (* Basic inversion lemmas ***************************************************)
 
-lemma sfr_inv_bind: ∀I,L,V,e. ≼ [0, e] L.ⓑ{I}V → 0 < e →
-                    ≼ [0, e - 1] L ∧ I = Abbr.
+lemma sfr_inv_bind: ∀I,L,V,e. ≽ [0, e] L.ⓑ{I}V → 0 < e →
+                    ≽ [0, e - 1] L ∧ I = Abbr.
 #I #L #V #e #HL #He
 lapply (HL (L.ⓓV) ?) /2 width=1/ #H
-elim (lsubs_inv_abbr1 … H ?) -H // #K #_ #H destruct
+elim (lsubs_inv_abbr2 … H ?) -H // #K #_ #H destruct
 @conj // #L #HKL
 lapply (HL (L.ⓓV) ?) -HL /2 width=1/ -HKL #H
-elim (lsubs_inv_abbr1 … H ?) -H // -He #X #HLX #H destruct //
+elim (lsubs_inv_abbr2 … H ?) -H // -He #X #HLX #H destruct //
 qed-.
 
-lemma sfr_inv_skip: ∀I,L,V,d,e. ≼ [d, e] L.ⓑ{I}V → 0 < d → ≼ [d - 1, e] L.
+lemma sfr_inv_skip: ∀I,L,V,d,e. ≽ [d, e] L.ⓑ{I}V → 0 < d → ≽ [d - 1, e] L.
 #I #L #V #d #e #HL #Hd #K #HLK
 lapply (HL (K.ⓑ{I}V) ?) -HL /2 width=1/ -HLK #H
-elim (lsubs_inv_skip1 … H ?) -H // -Hd #J #X #W #HKX #H destruct //
+elim (lsubs_inv_skip2 … H ?) -H // -Hd #J #X #W #HKX #H destruct //
 qed-.