- commit of the "substitution" component

- some renaming
- we disabled the old notation for ldrop to capture its instances
syntactically

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma
index 3656d36f66f42ec22e293262756ae6d41c85faa2..23cc4303177a20386435a58555b88baa89416691 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/acp_aaa.ma
@@ -36,7 +36,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
 | #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20
   lapply (aacr_acr … H1RP H2RP B) #HB
   elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct
-  lapply (ldrop_fwd_ldrop2 … HLK1) #HK1b
+  lapply (ldrop_fwd_drop2 … HLK1) #HK1b
   elim (ldrops_ldrop_trans … HL01 … HLK1) #X #des1 #i0 #HL0 #H #Hi0 #Hdes1
   >(at_mono … Hi1 … Hi0) -i1
   elim (ldrops_inv_skip2 … Hdes1 … H) -des1 #K0 #V0 #des0 #Hdes0 #HK01 #HV10 #H destruct
@@ -48,7 +48,7 @@ theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
     @(s5 … HB … (◊) … HV0 HLK2) /3 width=7 by ldrops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *)
   | -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0
     #K2 #V2 #A2 #HKV2A #H1KV0A #H2KV0A #_ #H1 #H2 destruct
-    lapply (ldrop_fwd_ldrop2 … HLK2) #HLK2b
+    lapply (ldrop_fwd_drop2 … HLK2) #HLK2b
     lapply (aaa_lifts … HK01 … HV10 HKV1B) -HKV1B -HK01 -HV10 #HKV0B
     lapply (aaa_mono … H2KV0A … HKV0B) #H destruct -H2KV0A -HKV0B
     elim (lift_total V0 0 (i0 +1)) #V3 #HV03

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma
index e570307acf0f7f875af1dd6044bb2e7e163a92ff..6298274bc74a5d7813dc0030af5f7df5dd236a70 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cprs_lift.ma
@@ -25,7 +25,7 @@ lemma cprs_delta: ∀G,L,K,V,V2,i.
                   ∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡* W2.
 #G #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=6/ ]
 #V1 #V2 #_ #HV12 #IHV1 #W2 #HVW2
-lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK
 elim (lift_total V1 0 (i+1)) /4 width=11 by cpr_lift, cprs_strap1/
 qed.
 
@@ -42,7 +42,7 @@ lemma cprs_inv_lref1: ∀G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡* T2 →
   elim (cpr_inv_lref1 … HT2) -HT2 /2 width=1/
   * /4 width=6/
 | * #K #V1 #T1 #HLK #HVT1 #HT1
-  lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
+  lapply (ldrop_fwd_drop2 … HLK) #H0LK
   elim (cpr_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T /4 width=6/
 ]
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
index fa14bfc252ecda088ae9cf658a292277f64db0ab..e4c5cea8459a398f33646ccfd9263bdc4a7b855f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
@@ -142,7 +142,7 @@ lemma fqu_cpxs_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2,
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
 [ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1)
   #U2 #HVU2 @(ex3_intro … U2)
-  [1,3: /3 width=7 by fqu_drop, cpxs_delta, ldrop_pair, ldrop_ldrop/
+  [1,3: /3 width=7 by fqu_drop, cpxs_delta, ldrop_pair, ldrop_drop/
   | #H destruct /2 width=7 by lift_inv_lref2_be/
   ]
 | #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T))

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
index 0c9cfe1e7b3e864b04fc17aea7e659cd987af06b..2d67976674c49b0249f1202604492f463fe81cd8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lift.ma
@@ -37,7 +37,7 @@ lemma cpxs_delta: ∀h,g,I,G,L,K,V,V2,i.
                   ∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃G, L⦄ ⊢ #i ➡*[h, g] W2.
 #h #g #I #G #L #K #V #V2 #i #HLK #H elim H -V2
 [ /3 width=9 by cpx_cpxs, cpx_delta/
-| #V1 lapply (ldrop_fwd_ldrop2 … HLK) -HLK
+| #V1 lapply (ldrop_fwd_drop2 … HLK) -HLK
   elim (lift_total V1 0 (i+1)) /4 width=11 by cpx_lift, cpxs_strap1/
 ]
 qed.
@@ -54,7 +54,7 @@ lemma cpxs_inv_lref1: ∀h,g,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡*[h, g] T2 →
   elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1 by or_introl/
   * /4 width=7 by cpx_cpxs, ex3_4_intro, or_intror/
 | * #I #K #V1 #T1 #HLK #HVT1 #HT1
-  lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
+  lapply (ldrop_fwd_drop2 … HLK) #H0LK
   elim (cpx_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T
   /4 width=7 by cpxs_strap1, ex3_4_intro, or_intror/
 ]

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
index faae2dd872941121a9a8bc82f64186de819602e3..30745dd38fe6db3fbfb88af72baeb9f084ea4acd 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_tstc.ma
@@ -64,7 +64,7 @@ lemma cpxs_fwd_delta: ∀h,g,I,G,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 →
 elim (cpxs_inv_lref1 … H) -H /2 width=1/
 * #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0
 lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct
-lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=9/
+lapply (ldrop_fwd_drop2 … HLK) -HLK /3 width=9/
 qed-.
 
 lemma cpxs_fwd_theta: ∀h,g,a,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ➡*[h, g] U →

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
index 5194bedfe8608992ec038876dd64a33d440c4c9b..4f06e7912938bf49280b8e7a83e40af1636a0f6f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_lift.ma
@@ -48,7 +48,7 @@ lemma csx_inv_lref_bind: ∀h,g,I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V →
                          ⦃G, L⦄ ⊢ ⬊*[h, g] #i → ⦃G, K⦄ ⊢ ⬊*[h, g] V.
 #h #g #I #G #L #K #V #i #HLK #Hi
 elim (lift_total V 0 (i+1))
-/4 width=9 by csx_inv_lift, csx_cpx_trans, cpx_delta, ldrop_fwd_ldrop2/
+/4 width=9 by csx_inv_lift, csx_cpx_trans, cpx_delta, ldrop_fwd_drop2/
 qed-.
 
 (* Advanced properties ******************************************************)
@@ -61,7 +61,7 @@ elim (cpx_inv_lref1 … H) -H
 [ #H destruct elim Hi //
 | -Hi * #I0 #K0 #V0 #V1 #HLK0 #HV01 #HV1
   lapply (ldrop_mono … HLK0 … HLK) -HLK #H destruct
-  /3 width=7 by csx_lift, csx_cpx_trans, ldrop_fwd_ldrop2/
+  /3 width=7 by csx_lift, csx_cpx_trans, ldrop_fwd_drop2/
 ]
 qed.
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
index f32a267c93c678a05d05fde0e75d4cd12b7ca1b4..e16b976a797067b40948fa927ab3837e8681f4d1 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_tstc_vector.ma
@@ -68,7 +68,7 @@ lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[0, i] L ≡ K.ⓑ{I}V1 →
                        ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.#i).
 #h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
 [ #H
-  lapply (ldrop_fwd_ldrop2 … HLK) #HLK0
+  lapply (ldrop_fwd_drop2 … HLK) #HLK0
   lapply (csx_inv_lift … H … HLK0 HV12) -V2 -HLK0 /2 width=5/
 | #V #Vs #IHV #H1T
   lapply (csx_fwd_pair_sn … H1T) #HV

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
index 10600383a97ccc1a1257208cbb2bf8ffc5127552..c961d137c61ee5f4d37b3adf20e1fdf5f5356968 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_cpxs.ma
@@ -77,7 +77,7 @@ lemma cpxs_inv_abbr1: ∀h,g,a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡*[h,
   ]
 | #U1 #HTU1 #HU01
   elim (lift_total U2 0 1) #U #HU2
-  /6 width=11 by cpxs_strap1, cpx_lift, ldrop_ldrop, ex3_intro, or_intror/
+  /6 width=11 by cpxs_strap1, cpx_lift, ldrop_drop, ex3_intro, or_intror/
 ]
 qed-.
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma
index 500d2f6879707b1b8dfaa5449b76c127fc97532e..8283ea54178ff728e7b79a19346ac2a996f0bd0c 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubsv_lsstas.ma
@@ -35,7 +35,7 @@ lemma lsubsv_lsstas_trans: ∀h,g,G,L2,T,U2,l1. ⦃G, L2⦄ ⊢ T •*[h, g, l1]
   elim (lsubsv_inv_pair2 … H) -H * #K1 [ | -HYU -IHXY -HLK1 ]
   [ #HK12 #H destruct
     elim (IHXY … Hl12 HV0 … HK12) -K2 -l2 #T #HXT #HTY
-    lapply (ldrop_fwd_ldrop2 … HLK1) #H
+    lapply (ldrop_fwd_drop2 … HLK1) #H
     elim (lift_total T 0 (i+1))
     /3 width=11 by lsstas_ldef, cpcs_lift, ex2_intro/
   | #V #l0 #_ #_ #_ #_ #_ #_ #_ #H destruct
@@ -50,7 +50,7 @@ lemma lsubsv_lsstas_trans: ∀h,g,G,L2,T,U2,l1. ⦃G, L2⦄ ⊢ T •*[h, g, l1]
     lapply (lsubsv_fwd_lsubd … HK12) #H
     lapply (lsubd_da_trans … HV0 … H) -H
     elim (IHXY … Hl12 HV0 … HK12) -K2 -Hl12 #Y0
-    lapply (ldrop_fwd_ldrop2 … HLK1)
+    lapply (ldrop_fwd_drop2 … HLK1)
     elim (lift_total Y0 0 (i+1))
     /3 width=11 by lsstas_ldec, cpcs_lift, ex2_intro/
   | #V #l #_ #_ #HVX #_ #HV #HX #HK12 #_ #H destruct
@@ -60,7 +60,7 @@ lemma lsubsv_lsstas_trans: ∀h,g,G,L2,T,U2,l1. ⦃G, L2⦄ ⊢ T •*[h, g, l1]
     elim (lsstas_total … HVW (l1+1)) -W #W #HVW
     lapply (HVX … Hl12 HVW HXY0) -HVX -Hl12 -HXY0 #HWY0
     lapply (cpcs_trans … HWY0 … HY0) -Y0
-    lapply (ldrop_fwd_ldrop2 … HLK1)
+    lapply (ldrop_fwd_drop2 … HLK1)
     elim (lift_total W 0 (i+1))
     /4 width=11 by lsstas_ldef, lsstas_cast, cpcs_lift, ex2_intro/
   ]

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
index b441376641b772377f207f64b92fb3b0ff861045..f86f5bd155d00a4b92e086eab4efe63f3fe29397 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_da_lpr.ma
@@ -45,7 +45,7 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0.
     lapply (fqup_lref … G1 … HLK1)
     elim (lpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2
     elim (lpr_inv_pair1 … H) -H #K2 #V2 #HK12 #_ #H destruct
-    lapply (ldrop_fwd_ldrop2 … HLK2) -V2
+    lapply (ldrop_fwd_drop2 … HLK2) -V2
     /4 width=7 by da_lift, fqup_fpbg/
   ]
 | #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1
@@ -57,7 +57,7 @@ fact da_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   [ #V2 #T2 #HV12 #HT12 #H destruct
     /4 width=9 by da_bind, fqup_fpbg, lpr_pair/
   | #T2 #HT12 #HT2 #H1 #H2 destruct
-    /4 width=11 by da_inv_lift, fqup_fpbg, lpr_pair, ldrop_ldrop/
+    /4 width=11 by da_inv_lift, fqup_fpbg, lpr_pair, ldrop_drop/
   ]
 | #V1 #T1 #HG0 #HL0 #HT0 #H1 #l #H2 #X3 #H3 #L2 #HL12 destruct
   elim (snv_inv_appl … H1) -H1 #b0 #W1 #W0 #T0 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HT10

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
index 60e0d261987d1120098d9f0924d85b4993940f38..75bf56d43aace00348e4eeb697fe3da5aca11e09 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lpr.ma
@@ -38,7 +38,7 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   [ #H destruct -HLK1 /4 width=10 by fqup_fpbg, snv_lref/
   | * #K0 #V0 #W0 #H #HVW0 #W0 -HV12
     lapply (ldrop_mono … H … HLK1) -HLK1 -H #H destruct
-    lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, snv_lift/
+    lapply (ldrop_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, snv_lift/
   ]
 | #p #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4 -IH3 -IH2 -IH1
   elim (snv_inv_gref … H1)
@@ -47,7 +47,7 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   elim (cpr_inv_bind1 … H2) -H2 *
   [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=8 by fqup_fpbg, snv_bind, lpr_pair/
   | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1
-    /4 width=10 by fqup_fpbg, snv_inv_lift, lpr_pair, ldrop_ldrop/
+    /4 width=10 by fqup_fpbg, snv_inv_lift, lpr_pair, ldrop_drop/
   ]
 | #V1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct
   elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU1
@@ -103,17 +103,17 @@ fact snv_cpr_lpr_aux: ∀h,g,G0,L0,T0.
     elim (ssta_cpr_lpr_aux … IH3 … HVW1 … HV10 … HL12) /2 width=2 by fqup_fpbg/ -IH3 -HVW1 #X #H1 #H2
     lapply (cpcs_canc_sn … H2 HW10) -W10 #H2
     elim (lift_total X 0 1) #W20 #H3
-    lapply (ssta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=1 by ldrop_ldrop/ -H1 #HVW20
-    lapply (cpcs_lift … (L2.ⓓW2) … H3 … HW13 H2) /2 width=1 by ldrop_ldrop/ -HW13 -H3 -H2 #HW320
+    lapply (ssta_lift … H1 (L2.ⓓW2) … HV02 … H3) /2 width=1 by ldrop_drop/ -H1 #HVW20
+    lapply (cpcs_lift … (L2.ⓓW2) … H3 … HW13 H2) /2 width=1 by ldrop_drop/ -HW13 -H3 -H2 #HW320
     lapply (cpcs_cprs_strap1 … HW320 … HW1) -W3 #HW20
     elim (cpcs_inv_cprs … HW20) -HW20 #W3 #HW203 #HW3
     lapply (cpds_cprs_trans … (ⓛ{a}W3.U2) HTU2 ?) /2 width=1 by cprs_bind/ -HW3 -HTU2 #HTU2
     lapply (IH2 … Hl0 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -IH2 -Hl0 #Hl0
-    lapply (da_lift … Hl0 (L2.ⓓW2) … HV02) /2 width=1 by ldrop_ldrop/ -Hl0 #Hl0
+    lapply (da_lift … Hl0 (L2.ⓓW2) … HV02) /2 width=1 by ldrop_drop/ -Hl0 #Hl0
     lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ -HW0 #HW2
     lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ -HV1 -HV10 #HV0
     lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -L1 #HT2
-    lapply (snv_lift … HV0 (L2.ⓓW2) … HV02) /3 width=7 by snv_bind, snv_appl, ldrop_ldrop/
+    lapply (snv_lift … HV0 (L2.ⓓW2) … HV02) /3 width=7 by snv_bind, snv_appl, ldrop_drop/
   ]
 | #W1 #T1 #HG0 #HL0 #HT0 #H1 #X #H2 #L2 #HL12 destruct -IH4
   elim (snv_inv_cast … H1) -H1 #U1 #l0 #HW1 #HT1 #Hl0 #HTU1 #HUW1

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma
index d13c47cd3ac1dfa04a85a90e2836a4289a9a2339..739caf494243bbfb50c41a4293dd65e66afe4288 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas.ma
@@ -37,7 +37,7 @@ fact snv_lsstas_aux: ∀h,g,G0,L0,T0.
   lapply (ldrop_mono … HLK0 … HLK1) -HLK0 #H destruct
   [ lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21 ]
   lapply (fqup_lref … G1 … HLK1) #H
-  lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 /4 width=8 by fqup_fpbg, snv_lift/
+  lapply (ldrop_fwd_drop2 … HLK1) -HLK1 /4 width=8 by fqup_fpbg, snv_lift/
 | #p #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2 -IH1
   elim (snv_inv_gref … H1)
 | #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X #H2 destruct -IH4 -IH3 -IH2

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma
index d43f443efa5d31f3753e00bd98d427e52c495934..a7b6e3e7787d4fb024865b02641bd3734ebd6946 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/snv_lsstas_lpr.ma
@@ -44,7 +44,7 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   lapply (fqup_lref … G1 … HLK1) #HKV1
   elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2
   elim (lpr_inv_pair1 … H) -H #K2 [ #W2 | #V2 ] #HK12 [ #HW12 | #HV12 ] #H destruct
-  lapply (ldrop_fwd_ldrop2 … HLK2) #H2
+  lapply (ldrop_fwd_drop2 … HLK2) #H2
   elim (cpr_inv_lref1 … H3) -H3
   [1,3: #H destruct -HLK1
   |2,4: * #K0 #V0 #X0 #H #HVX0 #HX0
@@ -73,7 +73,7 @@ fact lsstas_cpr_lpr_aux: ∀h,g,G0,L0,T0.
   | #T3 #HT13 #HXT3 #H1 #H2 destruct
     elim (IH1 … Hl1 … HTU1 … HT13 (L2.ⓓV1)) -IH1 -Hl1 -HTU1 -HT13 /2 width=1 by fqup_fpbg, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13
     elim (lsstas_inv_lift1 … HTU3 L2 … HXT3) -T3
-    /5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, ldrop_ldrop, ex2_intro/
+    /5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, ldrop_drop, ex2_intro/
   ]
 | #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct
   elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU10

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
index bc5044b6dfb379e0cc12fb09ab6b5bc38213b52a..0f015cc3202698bad360f7dd23a1deca8e4395d6 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx.ma
@@ -55,7 +55,7 @@ lemma lsubr_cpx_trans: ∀h,g,G. lsub_trans … (cpx h g G) lsubr.
 [ //
 | /2 width=2 by cpx_sort/
 | #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
-  elim (lsubr_fwd_ldrop2_bind … HL12 … HLK1) -HL12 -HLK1 *
+  elim (lsubr_fwd_drop2_bind … HL12 … HLK1) -HL12 -HLK1 *
   /4 width=7 by cpx_delta, cpx_ti/
 |4,9: /4 width=1 by cpx_bind, cpx_beta, lsubr_bind/
 |5,7,8: /3 width=1 by cpx_flat, cpx_tau, cpx_ti/
@@ -88,7 +88,7 @@ lemma cpx_delift: ∀h,g,I,G,K,V,T1,L,d. ⇩[0, d] L ≡ (K.ⓑ{I}V) →
   elim (lift_split … HVW i i) /3 width=7 by cpx_delta, ex2_2_intro/
 | * [ #a ] #I #W1 #U1 #IHW1 #IHU1 #L #d #HLK
   elim (IHW1 … HLK) -IHW1 #W2 #W #HW12 #HW2
-  [ elim (IHU1 (L. ⓑ{I} W1) (d+1)) -IHU1 /3 width=9 by cpx_bind, ldrop_ldrop, lift_bind, ex2_2_intro/
+  [ elim (IHU1 (L. ⓑ{I} W1) (d+1)) -IHU1 /3 width=9 by cpx_bind, ldrop_drop, lift_bind, ex2_2_intro/
   | elim (IHU1 … HLK) -IHU1 -HLK /3 width=8 by cpx_flat, lift_flat, ex2_2_intro/
   ]
 ]

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
index 505eabf1aebe1a86c2437ab05e6fa2d7ec304ead..4da4e21c844b9dee21d420652bb1f9cf1d5488c2 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
@@ -145,7 +145,7 @@ lemma fqu_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T
 /3 width=3 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, cpx_pair_sn, cpx_bind, cpx_flat, ex2_intro/
 [ #I #G #L #V2 #U2 #HVU2
   elim (lift_total U2 0 1)
-  /4 width=7 by fqu_drop, cpx_delta, ldrop_pair, ldrop_ldrop, ex2_intro/
+  /4 width=7 by fqu_drop, cpx_delta, ldrop_pair, ldrop_drop, ex2_intro/
 | #G #L #K #T1 #U1 #e #HLK1 #HTU1 #T2 #HTU2
   elim (lift_total T2 0 (e+1))
   /3 width=11 by cpx_lift, fqu_drop, ex2_intro/
@@ -200,7 +200,7 @@ lemma fqu_cpx_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
 [ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1)
   #U2 #HVU2 @(ex3_intro … U2)
-  [1,3: /3 width=7 by fqu_drop, cpx_delta, ldrop_pair, ldrop_ldrop/
+  [1,3: /3 width=7 by fqu_drop, cpx_delta, ldrop_pair, ldrop_drop/
   | #H destruct /2 width=7 by lift_inv_lref2_be/
   ]
 | #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T))

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
index bc56f721e72bf73ccc7d27ef1254704d29bc6343..d810ae1759c9ccf2e184b8ccb27f9d02fd4b331b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma
@@ -51,15 +51,15 @@ lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
 | /3 width=3 by lleq_fwd_length, lleq_sort/
 | #I2 #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #H elim (lleq_inv_lref_ge_dx … H … HLK2) // -H
   #I1 #K1 #HLK1 #HV1
-  lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 #HLK1
-  lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2
+  lapply (ldrop_fwd_drop2 … HLK1) -HLK1 #HLK1
+  lapply (ldrop_fwd_drop2 … HLK2) -HLK2 #HLK2
   @(lleq_lift_le … HLK1 HLK2 … HVW2) -HLK1 -HLK2 -HVW2 /2 width=1 by/ (**) (* full auto too slow *)
 | #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_bind_O … H) -H
   /4 width=5 by lleq_bind_repl_SO, lleq_bind/
 | #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
   /3 width=1 by lleq_flat/
 | #G #L2 #V #T1 #T2 #T #_ #HT2 #IHT12 #L1 #H elim (lleq_inv_bind_O … H) -H
-  /3 width=10 by lleq_inv_lift_le, ldrop_ldrop/
+  /3 width=10 by lleq_inv_lift_le, ldrop_drop/
 | #G #L2 #V #T1 #T2 #_ #IHT12 #L1 #H elim (lleq_inv_flat … H) -H /2 width=1 by/
 | #G #L2 #V1 #V2 #T #_ #IHV12 #L1 #H elim (lleq_inv_flat … H) -H /2 width=1 by/
 | #a #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
@@ -68,7 +68,7 @@ lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 →
 | #a #G #L2 #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H
   #HV1 #H elim (lleq_inv_bind_O … H) -H
   #HW1 #HT1 @lleq_bind_O /2 width=1 by/ @lleq_flat (**) (* full auto too slow *)
-  [ /3 width=10 by lleq_lift_le, ldrop_ldrop/
+  [ /3 width=10 by lleq_lift_le, ldrop_drop/
   | /3 width=3 by lleq_bind_repl_O/
 ]
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
index 933bcd6377f91b2e98ca2da43d869db32c2fe725..fb9e9e691702e315a50a67b9abb65be9f428de55 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr_lpr.ma
@@ -40,7 +40,7 @@ elim (lpr_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1
 elim (lpr_inv_pair1 … H1) -H1 #K1 #V1 #HK01 #HV01 #H destruct
 elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
 elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
-lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
+lapply (ldrop_fwd_drop2 … HLK2) -W2 #HLK2
 lapply (fqup_lref … G … HLK0) -HLK0 #HLK0
 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
 elim (lift_total V 0 (i+1))
@@ -66,10 +66,10 @@ fact cpr_conf_lpr_delta_delta:
 lapply (ldrop_mono … H … HLK0) -H #H destruct
 elim (lpr_ldrop_conf … HLK0 … HL01) -HL01 #X1 #H1 #HLK1
 elim (lpr_inv_pair1 … H1) -H1 #K1 #W1 #HK01 #_ #H destruct
-lapply (ldrop_fwd_ldrop2 … HLK1) -W1 #HLK1
+lapply (ldrop_fwd_drop2 … HLK1) -W1 #HLK1
 elim (lpr_ldrop_conf … HLK0 … HL02) -HL02 #X2 #H2 #HLK2
 elim (lpr_inv_pair1 … H2) -H2 #K2 #W2 #HK02 #_ #H destruct
-lapply (ldrop_fwd_ldrop2 … HLK2) -W2 #HLK2
+lapply (ldrop_fwd_drop2 … HLK2) -W2 #HLK2
 lapply (fqup_lref … G … HLK0) -HLK0 #HLK0
 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2
 elim (lift_total V 0 (i+1)) /3 width=11 by cpr_lift, ex2_intro/
@@ -107,7 +107,7 @@ fact cpr_conf_lpr_bind_zeta:
 #G #L0 #V0 #T0 #IH #V1 #HV01 #T1 #HT01
 #T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02
 elim (IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) -IH -HT01 -HT02 /2 width=1 by lpr_pair/ -L0 -V0 -T0 #T #HT1 #HT2
-elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /3 width=3 by cpr_zeta, ldrop_ldrop, ex2_intro/
+elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /3 width=3 by cpr_zeta, ldrop_drop, ex2_intro/
 qed-.
 
 fact cpr_conf_lpr_zeta_zeta:
@@ -124,8 +124,8 @@ fact cpr_conf_lpr_zeta_zeta:
 #G #L0 #V0 #T0 #IH #T1 #HT01 #X1 #HXT1
 #T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02
 elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 /2 width=1 by lpr_pair/ -L0 -T0 #T #HT1 #HT2
-elim (cpr_inv_lift1 … HT1 L1 … HXT1) -T1 /2 width=1 by ldrop_ldrop/ #T1 #HT1 #HXT1
-elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1 by ldrop_ldrop/ #T2 #HT2 #HXT2
+elim (cpr_inv_lift1 … HT1 L1 … HXT1) -T1 /2 width=1 by ldrop_drop/ #T1 #HT1 #HXT1
+elim (cpr_inv_lift1 … HT2 L2 … HXT2) -T2 /2 width=1 by ldrop_drop/ #T2 #HT2 #HXT2
 lapply (lift_inj … HT2 … HT1) -T #H destruct /2 width=3 by ex2_intro/
 qed-.
 
@@ -217,7 +217,7 @@ fact cpr_conf_lpr_flat_theta:
 #V2 #HV02 #U2 #HVU2 #W2 #HW02 #T2 #HT02 #L1 #HL01 #L2 #HL02
 elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2
 elim (lift_total V 0 1) #U #HVU
-lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1 by ldrop_ldrop/ #HU2
+lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1 by ldrop_drop/ #HU2
 elim (cpr_inv_abbr1 … H) -H *
 [ #W1 #T1 #HW01 #HT01 #H destruct
   elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/
@@ -226,7 +226,7 @@ elim (cpr_inv_abbr1 … H) -H *
 | #T1 #HT01 #HXT1 #H destruct
   elim (IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2
   elim (cpr_inv_lift1 … HT1 L1 … HXT1) -HXT1
-  /4 width=9 by cpr_flat, cpr_zeta, ldrop_ldrop, lift_flat, ex2_intro/
+  /4 width=9 by cpr_flat, cpr_zeta, ldrop_drop, lift_flat, ex2_intro/
 ]
 qed-.
 
@@ -271,8 +271,8 @@ elim (IH … HV01 … HV02 … HL01 … HL02) -HV01 -HV02 /2 width=1 by/ #V #HV1
 elim (IH … HW01 … HW02 … HL01 … HL02) /2 width=1 by/
 elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=1 by lpr_pair/ -L0 -V0 -W0 -T0
 elim (lift_total V 0 1) #U #HVU
-lapply (cpr_lift … HV1 (L1.ⓓW1) … HVU1 … HVU) -HVU1 /2 width=1 by ldrop_ldrop/
-lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1 by ldrop_ldrop/
+lapply (cpr_lift … HV1 (L1.ⓓW1) … HVU1 … HVU) -HVU1 /2 width=1 by ldrop_drop/
+lapply (cpr_lift … HV2 (L2.ⓓW2) … HVU2 … HVU) -HVU2 /2 width=1 by ldrop_drop/
 /4 width=7 by cpr_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *)
 qed-.
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
index e21810ea582ec56adb09cc452c207c4a37982768..3537c8d01af5e424142f2d4f4e303ef499d3582a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_aaa.ma
@@ -36,7 +36,7 @@ lemma aaa_cpx_lpx_conf: ∀h,g,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A →
     lapply (ldrop_mono … H … HLK1) -H #H destruct
     elim (lpx_ldrop_conf … HLK1 … HL12) -L1 #Z #H #HLK2
     elim (lpx_inv_pair1 … H) -H #K2 #V0 #HK12 #_ #H destruct
-    lapply (ldrop_fwd_ldrop2 … HLK2) -V0 /3 width=7/
+    lapply (ldrop_fwd_drop2 … HLK2) -V0 /3 width=7/
   ]
 | #a #G #L1 #V1 #T1 #B #A #_ #_ #IHV1 #IHT1 #X #H #L2 #HL12
   elim (cpx_inv_abbr1 … H) -H *

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
index 705d5695e3b2ff2e441bf37411e6bebaac1da058..b6c3584edcf5beee7d4340d25afd4d8cd319f815 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_ldrop.ma
@@ -61,7 +61,7 @@ lemma lpx_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T
 /3 width=7 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpx_pair, ex3_2_intro/
 [ #I #G1 #L1 #V1 #X #H elim (lpx_inv_pair2 … H) -H
   #K1 #W1 #HKL1 #HWV1 #H destruct elim (lift_total V1 0 1)
-  /4 width=7 by cpx_delta, fqu_drop, ldrop_ldrop, ex3_2_intro/
+  /4 width=7 by cpx_delta, fqu_drop, ldrop_drop, ex3_2_intro/
 | #G #L1 #K1 #T1 #U1 #e #HLK1 #HTU1 #L0 #HL01
   elim (lpx_ldrop_trans_O1 … HL01 … HLK1) -L1
   /3 width=5 by fqu_drop, ex3_2_intro/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
index b26b7e95b128caf163d94b776c92f82a106fcc7f..af0172fdb1e07f6913f4deb9715bf623e97e9522 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop.ma
@@ -36,11 +36,11 @@ inductive ldrop (s:bool): relation4 nat nat lenv lenv ≝
 interpretation
    "basic slicing (local environment) abstract"
    'RDrop s d e L1 L2 = (ldrop s d e L1 L2).
-
+(*
 interpretation
    "basic slicing (local environment) general"
    'RDrop d e L1 L2 = (ldrop true d e L1 L2).
-
+*)
 interpretation
    "basic slicing (local environment) lget"
    'RDrop e L1 L2 = (ldrop false O e L1 L2).

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma
index 45cf9cda7a73dbe6c710e2a03347df77dcbc5bb5..5cccd8fe1d6ccf11bd265c44dcb9cc131324b6cf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/aaa_ssta.ma
@@ -27,7 +27,7 @@ lemma aaa_ssta_conf: ∀h,g,G,L. Conf3 … (aaa G L) (ssta h g G L).
 | #I #G #L #K #V #B #i #HLK #HV #IHV #U #H
   elim (ssta_inv_lref1 … H) -H * #K0 #V0 #W0 #HLK0 #HVW0 #HU
   lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H0 destruct
-  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK
   @(aaa_lift … HLK … HU) -HU -L // -HV /2 width=2/
 | #a #G #L #V #T #B #A #HV #_ #_ #IHT #X #H
   elim (ssta_inv_bind1 … H) -H #U #HTU #H destruct /3 width=2/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma
index 94aec3b15d1f3a09bdf6bf7264ae7ca2a1b432c1..ff975d25a454e0bc0e59facd0dabba48343cdc09 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_lift.ma
@@ -108,11 +108,11 @@ lemma ssta_da_conf: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U →
 | #G #L #K #V #U #W #i #HLK #_ #HWU #IHVW #l #H
   elim (da_inv_lref … H) -H * #K0 #V0 [| #l0] #HLK0 #HV0
   lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct
-  lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=7/
+  lapply (ldrop_fwd_drop2 … HLK) -HLK /3 width=7/
 | #G #L #K #W #U #l0 #i #HLK #_ #HWU #l #H -l0
   elim (da_inv_lref … H) -H * #K0 #V0 [| #l1] #HLK0 #HV0 [| #H0 ]
   lapply (ldrop_mono … HLK0 … HLK) -HLK0 #H destruct
-  lapply (ldrop_fwd_ldrop2 … HLK) -HLK /3 width=7/
+  lapply (ldrop_fwd_drop2 … HLK) -HLK /3 width=7/
 | #a #I #G #L #V #T #U #_ #IHTU #l #H
   lapply (da_inv_bind … H) -H /3 width=1/
 | #G #L #V #T #U #_ #IHTU #l #H
@@ -129,11 +129,11 @@ lemma ssta_fwd_correct: ∀h,g,G,L,T,U. ⦃G, L⦄ ⊢ T •[h, g] U →
 #h #g #G #L #T #U #H elim H -G -L -T -U
 [ /2 width=2/
 | #G #L #K #V #U #W #i #HLK #_ #HWU * #T #HWT
-  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK
   elim (lift_total T 0 (i+1)) /3 width=10/
 | #G #L #K #W #U #l #i #HLK #HWl #HWU
   elim (da_ssta … HWl) -HWl #T #HWT
-  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK
   elim (lift_total T 0 (i+1)) /3 width=10/
 | #a #I #G #L #V #T #U #_ * /3 width=2/
 | #G #L #V #T #U #_ * #T0 #HUT0 /3 width=2/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
index 929007118c8ec26e2eaee90a189f6fc3a7c3462d..3fb179ed2922a458f7caf116f0086eca03b050ca 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma
@@ -21,7 +21,7 @@ include "basic_2/substitution/cpys_lift.ma".
 inductive cpysa: ynat → ynat → relation4 genv lenv term term ≝
 | cpysa_atom : ∀I,G,L,d,e. cpysa d e G L (⓪{I}) (⓪{I})
 | cpysa_subst: ∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → i < d+e →
-               ⇩[0, i] L ≡ K.ⓑ{I}V1 → cpysa 0 (⫰(d+e-i)) G K V1 V2 →
+               ⇩[i] L ≡ K.ⓑ{I}V1 → cpysa 0 (⫰(d+e-i)) G K V1 V2 →
                ⇧[0, i+1] V2 ≡ W2 → cpysa d e G L (#i) W2
 | cpysa_bind : ∀a,I,G,L,V1,V2,T1,T2,d,e.
                cpysa d e G L V1 V2 → cpysa (⫯d) e G (L.ⓑ{I}V2) T1 T2 →
@@ -58,7 +58,7 @@ lemma cpysa_cpy_trans: ∀G,L,T1,T,d,e. ⦃G, L⦄ ⊢ T1 ▶▶*×[d, e] T →
 [ #I #G #L #d #e #X #H
   elim (cpy_inv_atom1 … H) -H // * /2 width=7 by cpysa_subst/
 | #I #G #L #K #V1 #V2 #W2 #i #d #e #Hdi #Hide #HLK #_ #HVW2 #IHV12 #T2 #H
-  lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
+  lapply (ldrop_fwd_drop2 … HLK) #H0LK
   lapply (cpy_weak … H 0 (d+e) ? ?) -H // #H
   elim (cpy_inv_lift1_be … H … H0LK … HVW2) -H -H0LK -HVW2
   /3 width=7 by cpysa_subst, ylt_fwd_le_succ/
@@ -86,7 +86,7 @@ qed-.
 lemma cpys_ind_alt: ∀R:ynat→ynat→relation4 genv lenv term term.
                     (∀I,G,L,d,e. R d e G L (⓪{I}) (⓪{I})) →
                     (∀I,G,L,K,V1,V2,W2,i,d,e. d ≤ yinj i → i < d + e →
-                     ⇩[O, i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*×[O, ⫰(d+e-i)] V2 →
+                     ⇩[i] L ≡ K.ⓑ{I}V1 → ⦃G, K⦄ ⊢ V1 ▶*×[O, ⫰(d+e-i)] V2 →
                      ⇧[O, i+1] V2 ≡ W2 → R O (⫰(d+e-i)) G K V1 V2 → R d e G L (#i) W2
                     ) →
                     (∀a,I,G,L,V1,V2,T1,T2,d,e. ⦃G, L⦄ ⊢ V1 ▶*×[d, e] V2 →

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma
index aec0c7913345a9b47c34cbc8c0a3d4c0d7bafb99..a3eedc255b24a4dc5a3080c1e5899f2080be730e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma
@@ -59,11 +59,11 @@ lemma cpys_split_up: ∀G,L,T1,T2,d,e. ⦃G, L⦄ ⊢ T1 ▶*×[d, e] T2 →
 qed-.
 
 lemma cpys_inv_lift1_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
-                         ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
-                         d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
-                         ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[d, dt + et - (d + e)] T2 &
+                         ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                         d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et →
+                         ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[d, dt + et - (yinj d + e)] T2 &
                                ⇧[d, e] T2 ≡ U2.
-#G #L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
+#G #L #U1 #U2 #dt #et #HU12 #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
 elim (cpys_split_up … HU12 (d + e)) -HU12 // -Hdedet #U #HU1 #HU2
 lapply (cpys_weak … HU1 d e ? ?) -HU1 // [ >ymax_pre_sn_comm // ] -Hddt -Hdtde #HU1
 lapply (cpys_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma
index c4b9518e6c6f1595e02256a52fd228fe4ec42199..4a621d7d6653a82753fd6693456c460fca06bd0b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma
@@ -21,14 +21,14 @@ include "basic_2/substitution/cpys.ma".
 
 lemma cpys_subst: ∀I,G,L,K,V,U1,i,d,e.
                   d ≤ yinj i → i < d + e →
-                  ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*×[0, ⫰(d+e-i)] U1 →
+                  ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*×[0, ⫰(d+e-i)] U1 →
                   ∀U2. ⇧[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*×[d, e] U2.
 #I #G #L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(cpys_ind … H) -U1
 [ /3 width=5 by cpy_cpys, cpy_subst/
 | #U #U1 #_ #HU1 #IHU #U2 #HU12
   elim (lift_total U 0 (i+1)) #U0 #HU0
   lapply (IHU … HU0) -IHU #H
-  lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+  lapply (ldrop_fwd_drop2 … HLK) -HLK #HLK
   lapply (cpy_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // #HU02
   lapply (cpy_weak … HU02 d e ? ?) -HU02
   [2,3: /2 width=3 by cpys_strap1, yle_succ_dx/ ]
@@ -38,7 +38,7 @@ qed.
 
 lemma cpys_subst_Y2: ∀I,G,L,K,V,U1,i,d.
                      d ≤ yinj i →
-                     ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*×[0, ∞] U1 →
+                     ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, K⦄ ⊢ V ▶*×[0, ∞] U1 →
                      ∀U2. ⇧[0, i+1] U1 ≡ U2 → ⦃G, L⦄ ⊢ #i ▶*×[d, ∞] U2.
 #I #G #L #K #V #U1 #i #d #Hdi #HLK #HVU1 #U2 #HU12
 @(cpys_subst … HLK … HU12) >yminus_Y_inj //
@@ -49,7 +49,7 @@ qed.
 lemma cpys_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶*×[d, e] T2 →
                       T2 = ⓪{I} ∨
                       ∃∃J,K,V1,V2,i. d ≤ yinj i & i < d + e &
-                                    ⇩[O, i] L ≡ K.ⓑ{J}V1 &
+                                    ⇩[i] L ≡ K.ⓑ{J}V1 &
                                      ⦃G, K⦄ ⊢ V1 ▶*×[0, ⫰(d+e-i)] V2 &
                                      ⇧[O, i+1] V2 ≡ T2 &
                                      I = LRef i.
@@ -59,7 +59,7 @@ lemma cpys_inv_atom1: ∀I,G,L,T2,d,e. ⦃G, L⦄ ⊢ ⓪{I} ▶*×[d, e] T2 →
   [ #H destruct
     elim (cpy_inv_atom1 … HT2) -HT2 [ /2 width=1 by or_introl/ | * /3 width=11 by ex6_5_intro, or_intror/ ]
   | * #J #K #V1 #V #i #Hdi #Hide #HLK #HV1 #HVT #HI
-    lapply (ldrop_fwd_ldrop2 … HLK) #H
+    lapply (ldrop_fwd_drop2 … HLK) #H
     elim (cpy_inv_lift1_ge_up … HT2 … H … HVT) -HT2 -H -HVT
     [2,3,4: /2 width=1 by ylt_fwd_le_succ, yle_succ_dx/ ]
     /4 width=11 by cpys_strap1, ex6_5_intro, or_intror/
@@ -70,7 +70,7 @@ qed-.
 lemma cpys_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*×[d, e] T2 →
                       T2 = #i ∨
                       ∃∃I,K,V1,V2. d ≤ i & i < d + e &
-                                   ⇩[O, i] L ≡ K.ⓑ{I}V1 &
+                                   ⇩[i] L ≡ K.ⓑ{I}V1 &
                                    ⦃G, K⦄ ⊢ V1 ▶*×[0, ⫰(d+e-i)] V2 &
                                    ⇧[O, i+1] V2 ≡ T2.
 #G #L #T2 #i #d #e #H elim (cpys_inv_atom1 … H) -H /2 width=1 by or_introl/
@@ -78,7 +78,7 @@ lemma cpys_inv_lref1: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*×[d, e] T2 →
 qed-.
 
 lemma cpys_inv_lref1_ldrop: ∀G,L,T2,i,d,e. ⦃G, L⦄ ⊢ #i ▶*×[d, e] T2 →
-                            ∀I,K,V1. ⇩[O, i] L ≡ K.ⓑ{I}V1 →
+                            ∀I,K,V1. ⇩[i] L ≡ K.ⓑ{I}V1 →
                             ∀V2. ⇧[O, i+1] V2 ≡ T2 →
                             ∧∧ ⦃G, K⦄ ⊢ V1 ▶*×[0, ⫰(d+e-i)] V2
                              & d ≤ i
@@ -95,10 +95,10 @@ qed-.
 (* Properties on relocation *************************************************)
 
 lemma cpys_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 →
-                    ∀L,U1,d,e. dt + et ≤ yinj d → ⇩[d, e] L ≡ K →
+                    ∀L,U1,s,d,e. dt + et ≤ yinj d → ⇩[s, d, e] L ≡ K →
                     ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
                     ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2.
-#G #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdetd #HLK #HTU1 @(cpys_ind … H) -T2
+#G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hdetd #HLK #HTU1 @(cpys_ind … H) -T2
 [ #U2 #H >(lift_mono … HTU1 … H) -H //
 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
   elim (lift_total T d e) #U #HTU
@@ -108,10 +108,10 @@ lemma cpys_lift_le: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 →
 qed-.
 
 lemma cpys_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 →
-                    ∀L,U1,d,e. dt ≤ yinj d → d ≤ dt + et →
-                    ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 →
+                    ∀L,U1,s,d,e. dt ≤ yinj d → d ≤ dt + et →
+                    ⇩[s, d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 →
                     ∀U2. ⇧[d, e] T2 ≡ U2 → ⦃G, L⦄ ⊢ U1 ▶*×[dt, et + e] U2.
-#G #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 @(cpys_ind … H) -T2
+#G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hdtd #Hddet #HLK #HTU1 @(cpys_ind … H) -T2
 [ #U2 #H >(lift_mono … HTU1 … H) -H //
 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
   elim (lift_total T d e) #U #HTU
@@ -121,10 +121,10 @@ lemma cpys_lift_be: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 →
 qed-.
 
 lemma cpys_lift_ge: ∀G,K,T1,T2,dt,et. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 →
-                    ∀L,U1,d,e. yinj d ≤ dt → ⇩[d, e] L ≡ K →
+                    ∀L,U1,s,d,e. yinj d ≤ dt → ⇩[s, d, e] L ≡ K →
                     ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
                     ⦃G, L⦄ ⊢ U1 ▶*×[dt+e, et] U2.
-#G #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hddt #HLK #HTU1 @(cpys_ind … H) -T2
+#G #K #T1 #T2 #dt #et #H #L #U1 #s #d #e #Hddt #HLK #HTU1 @(cpys_ind … H) -T2
 [ #U2 #H >(lift_mono … HTU1 … H) -H //
 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
   elim (lift_total T d e) #U #HTU
@@ -136,10 +136,10 @@ qed-.
 (* Inversion lemmas for relocation ******************************************)
 
 lemma cpys_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
-                         ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                         ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
                          dt + et ≤ d →
                          ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et] T2 & ⇧[d, e] T2 ≡ U2.
-#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(cpys_ind … H) -U2
+#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdetd @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
   elim (cpy_inv_lift1_le … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
@@ -147,10 +147,10 @@ lemma cpys_inv_lift1_le: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2
 qed-.
 
 lemma cpys_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
-                         ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
-                         dt ≤ d → d + e ≤ dt + et →
+                         ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                         dt ≤ d → yinj d + e ≤ dt + et →
                          ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, et - e] T2 & ⇧[d, e] T2 ≡ U2.
-#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(cpys_ind … H) -U2
+#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
   elim (cpy_inv_lift1_be … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
@@ -158,10 +158,10 @@ lemma cpys_inv_lift1_be: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2
 qed-.
 
 lemma cpys_inv_lift1_ge: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
-                         ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
-                         d + e ≤ dt →
+                         ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                         yinj d + e ≤ dt →
                          ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt - e, et] T2 & ⇧[d, e] T2 ≡ U2.
-#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(cpys_ind … H) -U2
+#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdedt @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
   elim (cpy_inv_lift1_ge … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
@@ -171,11 +171,11 @@ qed-.
 (* Advanced inversion lemmas on relocation **********************************)
 
 lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
-                            ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
-                            d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
-                            ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[d, dt + et - (d + e)] T2 &
+                            ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                            d ≤ dt → dt ≤ yinj d + e → yinj d + e ≤ dt + et →
+                            ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[d, dt + et - (yinj d + e)] T2 &
                                  ⇧[d, e] T2 ≡ U2.
-#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(cpys_ind … H) -U2
+#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
   elim (cpy_inv_lift1_ge_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
@@ -183,10 +183,10 @@ lemma cpys_inv_lift1_ge_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et]
 qed-.
 
 lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
-                            ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
-                            dt ≤ d → dt + et ≤ d + e →
+                            ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                            dt ≤ d → dt + et ≤ yinj d + e →
                             ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2.
-#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(cpys_ind … H) -U2
+#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
   elim (cpy_inv_lift1_be_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/
@@ -194,10 +194,10 @@ lemma cpys_inv_lift1_be_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et]
 qed-.
 
 lemma cpys_inv_lift1_le_up: ∀G,L,U1,U2,dt,et. ⦃G, L⦄ ⊢ U1 ▶*×[dt, et] U2 →
-                            ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
-                            dt ≤ d → d ≤ dt + et → dt + et ≤ d + e →
+                            ∀K,s,d,e. ⇩[s, d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
+                            dt ≤ d → d ≤ dt + et → dt + et ≤ yinj d + e →
                             ∃∃T2. ⦃G, K⦄ ⊢ T1 ▶*×[dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2.
-#G #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(cpys_ind … H) -U2
+#G #L #U1 #U2 #dt #et #H #K #s #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(cpys_ind … H) -U2
 [ /2 width=3 by ex2_intro/
 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
   elim (cpy_inv_lift1_le_up … HU2 … HLK … HTU) -HU2 -HLK -HTU /3 width=3 by cpys_strap1, ex2_intro/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma
index 82a8f5ed00ba11072b01e109e23e3ee52ed5c0d9..e68fe729b677cc3de04a028dd9f25b84e43dd66b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup.ma
@@ -37,7 +37,7 @@ lemma fqup_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2.
                    ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄.
 /2 width=5 by tri_TC_strap/ qed.
 
-lemma fqup_ldrop: ∀G1,G2,L1,K1,K2,T1,T2,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 →
+lemma fqup_ldrop: ∀G1,G2,L1,K1,K2,T1,T2,U1,e. ⇩[e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 →
                   ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ → ⦃G1, L1, U1⦄ ⊃+ ⦃G2, K2, T2⦄.
 #G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #e #HLK1 #HTU1 #HT12 elim (eq_or_gt … e) #H destruct
 [ >(ldrop_inv_O2 … HLK1) -L1 <(lift_inv_O2 … HTU1) -U1 //
@@ -45,7 +45,7 @@ lemma fqup_ldrop: ∀G1,G2,L1,K1,K2,T1,T2,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e
 ]
 qed-.
 
-lemma fqup_lref: ∀I,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃+ ⦃G, K, V⦄.
+lemma fqup_lref: ∀I,G,L,K,V,i. ⇩[i] L ≡ K.ⓑ{I}V → ⦃G, L, #i⦄ ⊃+ ⦃G, K, V⦄.
 /3 width=6 by fqu_lref_O, fqu_fqup, lift_lref_ge, fqup_ldrop/ qed.
 
 lemma fqup_pair_sn: ∀I,G,L,V,T. ⦃G, L, ②{I}V.T⦄ ⊃+ ⦃G, L, V⦄.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma
index 325be4b397a4aff7c24d7e24480a4d46d074ccad..c05bb114531e3e1dec56a3ebbb38eea74628e196 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus.ma
@@ -56,7 +56,7 @@ lemma fqus_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G, L,
 /2 width=5 by tri_TC_strap/ qed-.
 
 lemma fqus_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ →
-                  ∀L1,U1,e. ⇩[0, e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 →
+                  ∀L1,U1,e. ⇩[e] L1 ≡ K1 → ⇧[0, e] T1 ≡ U1 →
                   ⦃G1, L1, U1⦄ ⊃* ⦃G2, K2, T2⦄.
 #G1 #G2 #K1 #K2 #T1 #T2 #H @(fqus_ind … H) -G2 -K2 -T2
 /3 width=5 by fqus_strap1, fquq_fqus, fquq_drop/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma
index 912487a44c309eaba230ee55d1cfb994c8f05604..868b8ec2aba8a541cae2bfbe1b5dc48c26a4725f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops.ma
@@ -13,53 +13,59 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/rdropstar_3.ma".
+include "basic_2/notation/relations/rdropstar_4.ma".
 include "basic_2/relocation/ldrop.ma".
 include "basic_2/substitution/gr2_minus.ma".
 include "basic_2/substitution/lifts.ma".
 
-(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
+(* ITERATED LOCAL ENVIRONMENT SLICING ***************************************)
 
-inductive ldrops: list2 nat nat → relation lenv ≝
-| ldrops_nil : ∀L. ldrops (⟠) L L
+inductive ldrops (s:bool): list2 nat nat → relation lenv ≝
+| ldrops_nil : ∀L. ldrops s (⟠) L L
 | ldrops_cons: ∀L1,L,L2,des,d,e.
-               ldrops des L1 L → ⇩[d,e] L ≡ L2 → ldrops ({d, e} @ des) L1 L2
+               ldrops s des L1 L → ⇩[s, d, e] L ≡ L2 → ldrops s ({d, e} @ des) L1 L2
 .
 
-interpretation "generic local environment slicing"
-   'RDropStar des T1 T2 = (ldrops des T1 T2).
+interpretation "iterated slicing (local environment) abstract"
+   'RDropStar s des T1 T2 = (ldrops s des T1 T2).
+(*
+interpretation "iterated slicing (local environment) general"
+   'RDropStar des T1 T2 = (ldrops true des T1 T2).
+*)
 
 (* Basic inversion lemmas ***************************************************)
 
-fact ldrops_inv_nil_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → des = ⟠ → L1 = L2.
-#L1 #L2 #des * -L1 -L2 -des //
+fact ldrops_inv_nil_aux: ∀L1,L2,s,des. ⇩*[s, des] L1 ≡ L2 → des = ⟠ → L1 = L2.
+#L1 #L2 #s #des * -L1 -L2 -des //
 #L1 #L #L2 #d #e #des #_ #_ #H destruct
 qed-.
 
 (* Basic_1: was: drop1_gen_pnil *)
-lemma ldrops_inv_nil: ∀L1,L2. ⇩*[⟠] L1 ≡ L2 → L1 = L2.
-/2 width=3 by ldrops_inv_nil_aux/ qed-.
+lemma ldrops_inv_nil: ∀L1,L2,s. ⇩*[s, ⟠] L1 ≡ L2 → L1 = L2.
+/2 width=4 by ldrops_inv_nil_aux/ qed-.
 
-fact ldrops_inv_cons_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 →
+fact ldrops_inv_cons_aux: ∀L1,L2,s,des. ⇩*[s, des] L1 ≡ L2 →
                           ∀d,e,tl. des = {d, e} @ tl →
-                          ∃∃L. ⇩*[tl] L1 ≡ L & ⇩[d, e] L ≡ L2.
-#L1 #L2 #des * -L1 -L2 -des
+                          ∃∃L. ⇩*[s, tl] L1 ≡ L & ⇩[s, d, e] L ≡ L2.
+#L1 #L2 #s #des * -L1 -L2 -des
 [ #L #d #e #tl #H destruct
 | #L1 #L #L2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct
   /2 width=3 by ex2_intro/
+]
 qed-.
 
 (* Basic_1: was: drop1_gen_pcons *)
-lemma ldrops_inv_cons: ∀L1,L2,d,e,des. ⇩*[{d, e} @ des] L1 ≡ L2 →
-                       ∃∃L. ⇩*[des] L1 ≡ L & ⇩[d, e] L ≡ L2.
+lemma ldrops_inv_cons: ∀L1,L2,s,d,e,des. ⇩*[s, {d, e} @ des] L1 ≡ L2 →
+                       ∃∃L. ⇩*[s, des] L1 ≡ L & ⇩[s, d, e] L ≡ L2.
 /2 width=3 by ldrops_inv_cons_aux/ qed-.
 
-lemma ldrops_inv_skip2: ∀I,des,i,des2. des ▭ i ≡ des2 →
-                        ∀L1,K2,V2. ⇩*[des2] L1 ≡ K2. ⓑ{I} V2 →
+lemma ldrops_inv_skip2: ∀I,s,des,des2,i. des ▭ i ≡ des2 →
+                        ∀L1,K2,V2. ⇩*[s, des2] L1 ≡ K2. ⓑ{I} V2 →
                         ∃∃K1,V1,des1. des + 1 ▭ i + 1 ≡ des1 + 1 &
-                                      ⇩*[des1] K1 ≡ K2 &
+                                      ⇩*[s, des1] K1 ≡ K2 &
                                       ⇧*[des1] V2 ≡ V1 &
                                       L1 = K1. ⓑ{I} V1.
-#I #des #i #des2 #H elim H -des -i -des2
+#I #s #des #des2 #i #H elim H -des -des2 -i
 [ #i #L1 #K2 #V2 #H
   >(ldrops_inv_nil … H) -L1 /2 width=7 by lifts_nil, minuss_nil, ex4_3_intro, ldrops_nil/
 | #des #des2 #d #e #i #Hid #_ #IHdes2 #L1 #K2 #V2 #H
@@ -77,9 +83,9 @@ qed-.
 (* Basic properties *********************************************************)
 
 (* Basic_1: was: drop1_skip_bind *)
-lemma ldrops_skip: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2 ≡ V1 →
-                   ∀I. ⇩*[des + 1] L1. ⓑ{I} V1 ≡ L2. ⓑ{I} V2.
-#L1 #L2 #des #H elim H -L1 -L2 -des
+lemma ldrops_skip: ∀L1,L2,s,des. ⇩*[s, des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2 ≡ V1 →
+                   ∀I. ⇩*[s, des + 1] L1.ⓑ{I}V1 ≡ L2.ⓑ{I}V2.
+#L1 #L2 #s #des #H elim H -L1 -L2 -des
 [ #L #V1 #V2 #HV12 #I
   >(lifts_inv_nil … HV12) -HV12 //
 | #L1 #L #L2 #des #d #e #_ #HL2 #IHL #V1 #V2 #H #I

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma
index 22eed845f8661e197299efba2e583cd3c63cc520..958052e5bd1108f57bd38d4df11bef17388a570b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrop.ma
@@ -15,21 +15,21 @@
 include "basic_2/relocation/ldrop_ldrop.ma".
 include "basic_2/substitution/ldrops.ma".
 
-(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
+(* ITERATED LOCAL ENVIRONMENT SLICING ***************************************)
 
 (* Properties concerning basic local environment slicing ********************)
 
-lemma ldrops_ldrop_trans: ∀L1,L,des. ⇩*[des] L1 ≡ L → ∀L2,i. ⇩[0, i] L ≡ L2 →
-                          ∃∃L0,des0,i0. ⇩[0, i0] L1 ≡ L0 & ⇩*[des0] L0 ≡ L2 &
+lemma ldrops_ldrop_trans: ∀L1,L,des. ⇩*[Ⓕ, des] L1 ≡ L → ∀L2,i. ⇩[i] L ≡ L2 →
+                          ∃∃L0,des0,i0. ⇩[i0] L1 ≡ L0 & ⇩*[Ⓕ, des0] L0 ≡ L2 &
                                         @⦃i, des⦄ ≡ i0 & des ▭ i ≡ des0.
 #L1 #L #des #H elim H -L1 -L -des
-[ /2 width=7/
+[ /2 width=7 by ldrops_nil, minuss_nil, at_nil, ex4_3_intro/
 | #L1 #L3 #L #des3 #d #e #_ #HL3 #IHL13 #L2 #i #HL2
   elim (lt_or_ge i d) #Hid
-  [ elim (ldrop_trans_le … HL3 … HL2) -L /2 width=2/ #L #HL3 #HL2
-    elim (IHL13 … HL3) -L3 /3 width=7/
+  [ elim (ldrop_trans_le … HL3 … HL2) -L /2 width=2 by lt_to_le/
+    #L #HL3 #HL2 elim (IHL13 … HL3) -L3 /3 width=7 by ldrops_cons, minuss_lt, at_lt, ex4_3_intro/
   | lapply (ldrop_trans_ge … HL3 … HL2 ?) -L // #HL32
-    elim (IHL13 … HL32) -L3 /3 width=7/
+    elim (IHL13 … HL32) -L3 /3 width=7 by minuss_ge, at_ge, ex4_3_intro/
   ]
 ]
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrops.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrops.ma
index a4dbfb02e435b4225612c649ddb3d6ff5e4db075..474862b8cf63efae03fda91da52813c3bdd933e5 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/ldrops_ldrops.ma
@@ -14,12 +14,12 @@
 
 include "basic_2/substitution/ldrops_ldrop.ma".
 
-(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
+(* ITERATED LOCAL ENVIRONMENT SLICING ***************************************)
 
 (* Main properties **********************************************************)
 
 (* Basic_1: was: drop1_trans *)
-theorem ldrops_trans: ∀L,L2,des2. ⇩*[des2] L ≡ L2 → ∀L1,des1. ⇩*[des1] L1 ≡ L →
-                      ⇩*[des2 @@ des1] L1 ≡ L2.
-#L #L2 #des2 #H elim H -L -L2 -des2 // /3 width=3/
-qed.
+theorem ldrops_trans: ∀L,L2,s,des2. ⇩*[s, des2] L ≡ L2 → ∀L1,des1. ⇩*[s, des1] L1 ≡ L →
+                      ⇩*[s, des2 @@ des1] L1 ≡ L2.
+#L #L2 #s #des2 #H elim H -L -L2 -des2 /3 width=3 by ldrops_cons/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
index 577343c6ecbac90fa244c071791078808f1d50ff..47d88486da3fcb7779a6c45ef21b3e2295826dae 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma
@@ -100,14 +100,14 @@ lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → |L1| = |L2|.
 #L1 #L2 #T #d * //
 qed-.
 
-lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K1,i. ⇩[0, i] L1 ≡ K1 →
-                         ∃K2. ⇩[0, i] L2 ≡ K2.
+lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K1,i. ⇩[i] L1 ≡ K1 →
+                         ∃K2. ⇩[i] L2 ≡ K2.
 #L1 #L2 #T #d #H #K1 #i #HLK1 lapply (lleq_fwd_length … H) -H
 #HL12 lapply (ldrop_fwd_length_le2 … HLK1) -HLK1 /2 width=1 by ldrop_O1_le/
 qed-.
 
-lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K2,i. ⇩[0, i] L2 ≡ K2 →
-                         ∃K1. ⇩[0, i] L1 ≡ K1.
+lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K2,i. ⇩[i] L2 ≡ K2 →
+                         ∃K1. ⇩[i] L1 ≡ K1.
 /3 width=6 by lleq_fwd_ldrop_sn, lleq_sym/ qed-.
 
 lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,d.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
index 0d99e8e1eee803774465ff77798e7fe2314d15ec..70bd0d615865179e8632c8332715304f38a8ebaa 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma
@@ -19,7 +19,7 @@ inductive lleqa: relation4 ynat term lenv lenv ≝
 | lleqa_sort: ∀L1,L2,d,k. |L1| = |L2| → lleqa d (⋆k) L1 L2
 | lleqa_skip: ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → lleqa d (#i) L1 L2
 | lleqa_lref: ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
-              ⇩[0, i] L1 ≡ K1.ⓑ{I1}V → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V →
+              ⇩[i] L1 ≡ K1.ⓑ{I1}V → ⇩[i] L2 ≡ K2.ⓑ{I2}V →
               lleqa (yinj 0) V K1 K2 → lleqa d (#i) L1 L2
 | lleqa_free: ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → lleqa d (#i) L1 L2
 | lleqa_gref: ∀L1,L2,d,p. |L1| = |L2| → lleqa d (§p) L1 L2
@@ -61,7 +61,7 @@ lemma lleq_ind_alt: ∀R:relation4 ynat term lenv lenv. (
                        ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → R d (#i) L1 L2
                     ) → (
                        ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
-                       ⇩[O, i] L1 ≡ K1.ⓑ{I1}V → ⇩[O, i] L2 ≡ K2.ⓑ{I2}V →
+                       ⇩[i] L1 ≡ K1.ⓑ{I1}V → ⇩[i] L2 ≡ K2.ⓑ{I2}V →
                        K1 ⋕[V, yinj O] K2 → R (yinj O) V K1 K2 → R d (#i) L1 L2
                     ) → (
                        ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → R d (#i) L1 L2

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma
index a1cf4458d64ecdf5d821a102ab2d34ad4fd86f36..d6bb03fa7c799e8d14830bea95e5755ec7a473f4 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma
@@ -19,7 +19,7 @@ include "basic_2/substitution/lleq_alt.ma".
 (* Advanced inversion lemmas ************************************************)
 
 fact lleq_inv_S_aux: ∀L1,L2,T,d0. L1 ⋕[T, d0] L2 → ∀d. d0 = d + 1 →
-                     ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V →
+                     ∀K1,K2,I,V. ⇩[d] L1 ≡ K1.ⓑ{I}V → ⇩[d] L2 ≡ K2.ⓑ{I}V →
                      K1 ⋕[V, 0] K2 → L1 ⋕[T, d] L2.
 #L1 #L2 #T #d0 #H @(lleq_ind_alt … H) -L1 -L2 -T -d0
 /2 width=1 by lleq_gref, lleq_free, lleq_sort/
@@ -29,14 +29,14 @@ fact lleq_inv_S_aux: ∀L1,L2,T,d0. L1 ⋕[T, d0] L2 → ∀d. d0 = d + 1 →
 | #I1 #I2 #L1 #L2 #K11 #K22 #V #d0 #i #Hd0i #HLK11 #HLK22 #HV #_ #d #H #K1 #K2 #J #W #_ #_ #_ destruct
   /3 width=8 by lleq_lref, yle_pred_sn/
 | #a #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct
-  /4 width=7 by lleq_bind, ldrop_ldrop/
+  /4 width=7 by lleq_bind, ldrop_drop/
 | #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct
   /3 width=7 by lleq_flat/
 ]
 qed-.
 
 lemma lleq_inv_S: ∀T,L1,L2,d. L1 ⋕[T, d+1] L2 →
-                  ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V →
+                  ∀K1,K2,I,V. ⇩[d] L1 ≡ K1.ⓑ{I}V → ⇩[d] L2 ≡ K2.ⓑ{I}V →
                   K1 ⋕[V, 0] K2 → L1 ⋕[T, d] L2.
 /2 width=7 by lleq_inv_S_aux/ qed-.
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma
index 126da3dd362571f9dfd49f686a2a8dc78681c389..9cb597c6f7be12cff7ac7a055962fd37bb424fd0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma
@@ -26,7 +26,7 @@ lemma lleq_skip: ∀L1,L2,d,i. yinj i < d → |L1| = |L2| → L1 ⋕[#i, d] L2.
 qed.
 
 lemma lleq_lref: ∀I1,I2,L1,L2,K1,K2,V,d,i. d ≤ yinj i →
-                 ⇩[0, i] L1 ≡ K1.ⓑ{I1}V → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V →
+                 ⇩[i] L1 ≡ K1.ⓑ{I1}V → ⇩[i] L2 ≡ K2.ⓑ{I2}V →
                  K1 ⋕[V, 0] K2 → L1 ⋕[#i, d] L2.
 #I1 #I2 #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #HLK2 * #HK12 #IH @conj [ -IH | -HK12 ]
 [ lapply (ldrop_fwd_length … HLK1) -HLK1 #H1
@@ -50,31 +50,31 @@ qed.
 (* Properties on relocation *************************************************)
 
 lemma lleq_lift_le: ∀K1,K2,T,dt. K1 ⋕[T, dt] K2 →
-                    ∀L1,L2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+                    ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 →
                     ∀U. ⇧[d, e] T ≡ U → dt ≤ d → L1 ⋕[U, dt] L2.
 #K1 #K2 #T #dt * #HK12 #IHT #L1 #L2 #d #e #HLK1 #HLK2 #U #HTU #Hdtd
 lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2)
 #H2 #H1 @conj // -HK12 -H1 -H2 #U0 @conj #HU0
 [ letin HLKA ≝ HLK1 letin HLKB ≝ HLK2 | letin HLKA ≝ HLK2 letin HLKB ≝ HLK1 ]
 elim (cpys_inv_lift1_be … HU0 … HLKA … HTU) // -HU0 >yminus_Y_inj #T0 #HT0 #HTU0
-elim (IHT T0) [ #H #_ | #_ #H ] -IHT /3 width=11 by cpys_lift_be/
+elim (IHT T0) [ #H #_ | #_ #H ] -IHT /3 width=12 by cpys_lift_be/
 qed-.
 
 lemma lleq_lift_ge: ∀K1,K2,T,dt. K1 ⋕[T, dt] K2 →
-                    ∀L1,L2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+                    ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 →
                     ∀U. ⇧[d, e] T ≡ U → d ≤ dt → L1 ⋕[U, dt+e] L2.
 #K1 #K2 #T #dt * #HK12 #IHT #L1 #L2 #d #e #HLK1 #HLK2 #U #HTU #Hddt
 lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2)
 #H2 #H1 @conj // -HK12 -H1 -H2 #U0 @conj #HU0
 [ letin HLKA ≝ HLK1 letin HLKB ≝ HLK2 | letin HLKA ≝ HLK2 letin HLKB ≝ HLK1 ]
 elim (cpys_inv_lift1_ge … HU0 … HLKA … HTU) /2 width=1 by monotonic_yle_plus_dx/ -HU0 >yplus_minus_inj #T0 #HT0 #HTU0
-elim (IHT T0) [ #H #_ | #_ #H ] -IHT /3 width=9 by cpys_lift_ge/
+elim (IHT T0) [ #H #_ | #_ #H ] -IHT /3 width=10 by cpys_lift_ge/
 qed-.
 
 (* Inversion lemmas on relocation *******************************************)
 
 lemma lleq_inv_lift_le: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 →
-                        ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
+                        ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 →
                         ∀T. ⇧[d, e] T ≡ U → dt ≤ d → K1 ⋕[T, dt] K2.
 #L1 #L2 #U #dt * #HL12 #IH #K1 #K2 #d #e #HLK1 #HLK2 #T #HTU #Hdtd
 lapply (ldrop_fwd_length_minus2 … HLK1) lapply (ldrop_fwd_length_minus2 … HLK2)
@@ -89,8 +89,8 @@ lapply (cpys_lift_be … HT0 … HLKA … HTU … HTU0) // -HT0
 qed-.
 
 lemma lleq_inv_lift_ge: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 →
-                        ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
-                        ∀T. ⇧[d, e] T ≡ U → d+e ≤ dt → K1 ⋕[T, dt-e] K2.
+                        ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 →
+                        ∀T. ⇧[d, e] T ≡ U → yinj d + e ≤ dt → K1 ⋕[T, dt-e] K2.
 #L1 #L2 #U #dt * #HL12 #IH #K1 #K2 #d #e #HLK1 #HLK2 #T #HTU #Hdedt
 lapply (ldrop_fwd_length_minus2 … HLK1) lapply (ldrop_fwd_length_minus2 … HLK2)
 #H2 #H1 @conj // -HL12 -H1 -H2
@@ -105,8 +105,8 @@ lapply (cpys_lift_ge … HT0 … HLKA … HTU … HTU0) // -HT0 -Hddt
 qed-.
 
 lemma lleq_inv_lift_be: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 →
-                        ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 →
-                        ∀T. ⇧[d, e] T ≡ U → d ≤ dt → dt ≤ d + e → K1 ⋕[T, d] K2.
+                        ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 →
+                        ∀T. ⇧[d, e] T ≡ U → d ≤ dt → dt ≤ yinj d + e → K1 ⋕[T, d] K2.
 #L1 #L2 #U #dt * #HL12 #IH #K1 #K2 #d #e #HLK1 #HLK2 #T #HTU #Hddt #Hdtde
 lapply (ldrop_fwd_length_minus2 … HLK1) lapply (ldrop_fwd_length_minus2 … HLK2)
 #H2 #H1 @conj // -HL12 -H1 -H2

diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
index 97f2dd675a7e4ad87aef9fa3beec4706d070f4d7..01e08e9f9124939a65113db0fd3a883a9017cf3f 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma
@@ -20,8 +20,8 @@ include "basic_2/substitution/lleq_ldrop.ma".
 lemma lleq_fwd_lref: ∀L1,L2. ∀d:ynat. ∀i:nat. L1 ⋕[#i, d] L2 →
                      ∨∨ |L1| ≤ i ∧ |L2| ≤ i
                       | yinj i < d
-                      | ∃∃I1,I2,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V &
-                                         ⇩[0, i] L2 ≡ K2.ⓑ{I2}V &
+                      | ∃∃I1,I2,K1,K2,V. ⇩[i] L1 ≡ K1.ⓑ{I1}V &
+                                         ⇩[i] L2 ≡ K2.ⓑ{I2}V &
                                          K1 ⋕[V, yinj 0] K2 & d ≤ yinj i.
 #L1 #L2 #d #i * #HL12 #IH elim (lt_or_ge i (|L1|)) /3 width=3 by or3_intro0, conj/
 elim (ylt_split i d) /2 width=1 by or3_intro1/ #Hdi #Hi
@@ -46,9 +46,9 @@ lapply (cpys_antisym_eq … H12 … H21) -H12 -H21 #H destruct
 qed-.
 
 lemma lleq_fwd_lref_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 →
-                        ∀I2,K2,V. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V →
+                        ∀I2,K2,V. ⇩[i] L2 ≡ K2.ⓑ{I2}V →
                         i < d ∨
-                        ∃∃I1,K1. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V & K1 ⋕[V, 0] K2 & d ≤ i.
+                        ∃∃I1,K1. ⇩[i] L1 ≡ K1.ⓑ{I1}V & K1 ⋕[V, 0] K2 & d ≤ i.
 #L1 #L2 #d #i #H #I2 #K2 #V #HLK2 elim (lleq_fwd_lref … H) -H [ * || * ]
 [ #_ #H elim (lt_refl_false i)
   lapply (ldrop_fwd_length_lt2 … HLK2) -HLK2
@@ -60,9 +60,9 @@ lemma lleq_fwd_lref_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 →
 qed-.
 
 lemma lleq_fwd_lref_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 →
-                        ∀I1,K1,V. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V →
+                        ∀I1,K1,V. ⇩[i] L1 ≡ K1.ⓑ{I1}V →
                         i < d ∨
-                        ∃∃I2,K2. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V & K1 ⋕[V, 0] K2 & d ≤ i.
+                        ∃∃I2,K2. ⇩[i] L2 ≡ K2.ⓑ{I2}V & K1 ⋕[V, 0] K2 & d ≤ i.
 #L1 #L2 #d #i #HL12 #I1 #K1 #V #HLK1 elim (lleq_fwd_lref_dx L2 … d … HLK1) -HLK1
 [2: * ] /4 width=6 by lleq_sym, ex3_2_intro, or_introl, or_intror/
 qed-.
@@ -70,8 +70,8 @@ qed-.
 (* Advanced inversion lemmas ************************************************)
 
 lemma lleq_inv_lref_ge_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
-                           ∀I2,K2,V. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V →
-                           ∃∃I1,K1. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V & K1 ⋕[V, 0] K2.
+                           ∀I2,K2,V. ⇩[i] L2 ≡ K2.ⓑ{I2}V →
+                           ∃∃I1,K1. ⇩[i] L1 ≡ K1.ⓑ{I1}V & K1 ⋕[V, 0] K2.
 #L1 #L2 #d #i #H #Hdi #I2 #K2 #V #HLK2 elim (lleq_fwd_lref_dx … H … HLK2) -L2
 [ #H elim (ylt_yle_false … H Hdi)
 | * /2 width=4 by ex2_2_intro/
@@ -79,8 +79,8 @@ lemma lleq_inv_lref_ge_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
 qed-.
 
 lemma lleq_inv_lref_ge_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i →
-                           ∀I1,K1,V. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V →
-                           ∃∃I2,K2. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V & K1 ⋕[V, 0] K2.
+                           ∀I1,K1,V. ⇩[i] L1 ≡ K1.ⓑ{I1}V →
+                           ∃∃I2,K2. ⇩[i] L2 ≡ K2.ⓑ{I2}V & K1 ⋕[V, 0] K2.
 #L1 #L2 #d #i #HL12 #Hdi #I1 #K1 #V #HLK1 elim (lleq_inv_lref_ge_dx L2 … Hdi … HLK1) -Hdi -HLK1
 /3 width=4 by lleq_sym, ex2_2_intro/
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma
index 3019423b46a04080501faef87647897c8ed25872..6fab6dec640d242cc4733df1317062ac093c60a0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_alt.ma
@@ -47,10 +47,10 @@ lemma lsstasa_step_dx: ∀h,g,G,L,T1,T,l. ⦃G, L⦄ ⊢ T1 ••*[h, g, l] T 
 [ /2 width=1/
 | #G #L #l #k #X #H >(ssta_inv_sort1 … H) -X >commutative_plus //
 | #G #L #K #V #W #U #i #l #HLK #_ #HWU #IHVW #U2 #HU2
-  lapply (ldrop_fwd_ldrop2 … HLK) #H
+  lapply (ldrop_fwd_drop2 … HLK) #H
   elim (ssta_inv_lift1 … HU2 … H … HWU) -H -U /3 width=6/
 | #G #L #K #W #V #U #i #l #l0 #HLK #HWl0 #_ #HVU #IHWV #U2 #HU2
-  lapply (ldrop_fwd_ldrop2 … HLK) #H
+  lapply (ldrop_fwd_drop2 … HLK) #H
   elim (ssta_inv_lift1 … HU2 … H … HVU) -H -U /3 width=8/
 | #a #I #G #L #V #T1 #U1 #l #_ #IHTU1 #X #H
   elim (ssta_inv_bind1 … H) -H #U #HU1 #H destruct /3 width=1/

diff --git a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma
index c4c27e9fdeb55fe5c0eabea31c359631d9a0628b..76c9c27f3e14c4cc27db6be48064aba5859ef7bc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/unfold/lsstas_lift.ma
@@ -39,7 +39,7 @@ lemma lsstas_inv_lref1: ∀h,g,G,L,U,i,l. ⦃G, L⦄ ⊢ #i •*[h, g, l+1] U 
 #h #g #G #L #U #i #l #H elim (lsstas_inv_step_sn … H) -H
 #X #H #HXU elim (ssta_inv_lref1 … H) -H
 * #K [ #V #W | #W #l0 ] #HLK [ #HVW | #HWl0 ] #HWX
-lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
+lapply (ldrop_fwd_drop2 … HLK) #H0LK
 elim (lsstas_inv_lift1 … HXU … H0LK … HWX) -H0LK -X /3 width=8/ /4 width=6/
 qed-.
 
@@ -66,7 +66,7 @@ lemma lsstas_ldef: ∀h,g,G,L,K,V,i. ⇩[0, i] L ≡ K.ⓓV →
                    ∀W,l. ⦃G, K⦄ ⊢ V •*[h, g, l+1] W →
                    ∀U. ⇧[0, i+1] W ≡ U → ⦃G, L⦄ ⊢ #i •*[h, g, l+1] U.
 #h #g #G #L #K #V #i #HLK #W #l #HVW #U #HWU
-lapply (ldrop_fwd_ldrop2 … HLK)
+lapply (ldrop_fwd_drop2 … HLK)
 elim (lsstas_inv_step_sn … HVW) -HVW #W0
 elim (lift_total W0 0 (i+1)) /3 width=11/
 qed.
@@ -75,7 +75,7 @@ lemma lsstas_ldec: ∀h,g,G,L,K,W,i. ⇩[0, i] L ≡ K.ⓛW → ∀l0. ⦃G, K
                    ∀V,l. ⦃G, K⦄ ⊢ W •*[h, g, l] V →
                    ∀U. ⇧[0, i+1] V ≡ U → ⦃G, L⦄ ⊢ #i •*[h, g, l+1] U.
 #h #g #G #L #K #W #i #HLK #T #HWT #V #l #HWV #U #HVU
-lapply (ldrop_fwd_ldrop2 … HLK) #H
+lapply (ldrop_fwd_drop2 … HLK) #H
 elim (lift_total W 0 (i+1)) /3 width=11/
 qed.
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index da58e39aadd41a912edb61a5bee431ce2762dd25..d2d8186afda97936ddd4a8efa0a2d48ff67c8341 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -221,7 +221,7 @@ table {
              [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_fqup" * ]
           }
         ]
-        [ { "generic local env. slicing" * } {
+        [ { "iterated local env. slicing" * } {
              [ "ldrops ( ⇩*[?,?] ? ≡ ? )" "ldrops_ldrop" + "ldrops_ldrops" * ]
           }
         ]