uncommited file found :)

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / unfold / delift_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma
index 2591509095f4d0587111c85d2ab8b99dcac5f0e6..8abaeb9f9cc5f93137d821e7ad24bd7b86775359 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/delift_lift.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/substitution/ldrop_sfr.ma".
+include "basic_2/substitution/ldrop_lbotr.ma".
 include "basic_2/unfold/tpss_lift.ma".
 include "basic_2/unfold/delift.ma".
 
@@ -25,13 +25,13 @@ lemma delift_lref_be: ∀L,K,V1,V2,U2,i,d,e. d ≤ i → i < d + e →
                       ⇧[0, d] V2 ≡ U2 → L ⊢ ▼*[d, e] #i ≡ U2.
 #L #K #V1 #V2 #U2 #i #d #e #Hdi #Hide #HLK * #V #HV1 #HV2 #HVU2
 elim (lift_total V 0 (i+1)) #U #HVU
-lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus <plus_minus_m_m /2 width=1/ #HV2U 
+lapply (lift_trans_be … HV2 … HVU ? ?) -HV2 // >minus_plus <plus_minus_m_m /2 width=1/ #HV2U
 lapply (lift_conf_be … HVU2 … HV2U ?) //
 >commutative_plus in ⊢ (??%??→?); <minus_plus_m_m /3 width=6/
 qed.
 
-lemma sfr_delift: ∀L,T1,d,e. d + e ≤ |L| → ≽ [d, e] L →
-                  ∃T2. L ⊢ ▼*[d, e] T1 ≡ T2.
+lemma lbotr_delift: ∀L,T1,d,e. d + e ≤ |L| → ⊒[d, e] L →
+                    ∃T2. L ⊢ ▼*[d, e] T1 ≡ T2.
 #L #T1 @(f2_ind … fw … L T1) -L -T1
 #n #IH #L * * /2 width=2/
 [ #i #H #d #e #Hde #HL destruct
@@ -39,11 +39,11 @@ lemma sfr_delift: ∀L,T1,d,e. d + e ≤ |L| → ≽ [d, e] L →
   elim (lt_or_ge i (d+e)) #Hide [2: /3 width=2/ ]
   lapply (lt_to_le_to_lt … Hide Hde) #Hi
   elim (ldrop_O1_lt … Hi) -Hi #I #K #V1 #HLK
-  lapply (sfr_inv_ldrop … HLK … HL ? ?) // #H destruct
+  lapply (lbotr_inv_ldrop … HLK … HL ? ?) // #H destruct
   lapply (ldrop_pair2_fwd_fw … HLK (#i)) #HKL
   lapply (ldrop_fwd_ldrop2 … HLK) #HLK0
   lapply (ldrop_fwd_O1_length … HLK0) #H
-  lapply (sfr_ldrop_trans_be_up … HLK0 … HL ? ?) -HLK0 -HL
+  lapply (lbotr_ldrop_trans_be_up … HLK0 … HL ? ?) -HLK0 -HL
   [1,2: /2 width=1/ | <minus_n_O <minus_plus ] #HK
   elim (IH … HKL … HK) -IH -HKL -HK
   [2: >H -H /2 width=1/ ] -Hde -H #V2 #V12 (**) (* H erased two times *)
@@ -51,7 +51,7 @@ lemma sfr_delift: ∀L,T1,d,e. d + e ≤ |L| → ≽ [d, e] L →
 | #a #I #V1 #T1 #H #d #e #Hde #HL destruct
   elim (IH … V1 … Hde HL) // #V2 #HV12
   elim (IH (L.ⓑ{I}V1) T1 … (d+1) e ??) -IH // [2,3: /2 width=1/ ] -Hde -HL #T2 #HT12
-  lapply (delift_lsubs_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/ /3 width=4/
+  lapply (delift_lsubr_trans … HT12 (L.ⓑ{I}V2) ?) -HT12 /2 width=1/ /3 width=4/
 | #I #V1 #T1 #H #d #e #Hde #HL destruct
   elim (IH … V1 … Hde HL) // #V2 #HV12
   elim (IH … T1 … Hde HL) -IH -Hde -HL // /3 width=2/
@@ -95,7 +95,7 @@ elim (tpss_inv_lref1 … HU) -HU
 qed-.
 
 lemma delift_inv_lref1: ∀L,U2,i,d,e. L ⊢ ▼*[d, e] #i ≡ U2 →
-                        ∨∨ (i < d ∧ U2 = #i) 
+                        ∨∨ (i < d ∧ U2 = #i)
                         |  (∃∃K,V1,V2. d ≤ i & i < d + e &
                                        ⇩[0, i] L ≡ K. ⓓV1 &
                                        K ⊢ ▼*[0, d + e - i - 1] V1 ≡ V2 &