- predefined_virtuals: an addition

[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / substitution / lsubs_sfr.ma

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 fb71a175c4b3d73d7c4af780e5f83b324f9039ad..2b71621faf2ba690f8342347c570930034186d01 100644 (file)
--- 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,53 @@ 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: â\88\80d,e. â\89¼ [d, e] ⋆.
+lemma sfr_atom: â\88\80d,e. â\89½ [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: â\88\80L. â\89¼ [0, 0] L.
+lemma sfr_OO: â\88\80L. â\89½ [0, 0] L.
 // qed.
 
-lemma sfr_abbr: â\88\80L,V,e. â\89¼ [0, e] L â\86\92 â\89¼ [0, e + 1] L.ⓓV.
+lemma sfr_abbr: â\88\80L,V,e. â\89½ [0, e] L â\86\92 â\89½ [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: â\88\80I,L,V,d,e. â\89¼ [d, e] L â\86\92 â\89¼ [d + 1, e] L.ⓑ{I}V.
+lemma sfr_skip: â\88\80I,L,V,d,e. â\89½ [d, e] L â\86\92 â\89½ [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: â\88\80I,L,V,e. â\89¼ [0, e] L.ⓑ{I}V → 0 < e →
-                    â\89¼ [0, e - 1] L ∧ I = Abbr.
+lemma sfr_inv_bind: â\88\80I,L,V,e. â\89½ [0, e] L.ⓑ{I}V → 0 < e →
+                    â\89½ [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: â\88\80I,L,V,d,e. â\89¼ [d, e] L.â\93\91{I}V â\86\92 0 < d â\86\92 â\89¼ [d - 1, e] L.
+lemma sfr_inv_skip: â\88\80I,L,V,d,e. â\89½ [d, e] L.â\93\91{I}V â\86\92 0 < d â\86\92 â\89½ [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-.