From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 19 Feb 2017 15:32:41 +0000 (+0000)
Subject: support for generic reducibility ...
X-Git-Tag: make_still_working~502
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9be6753b7f120a4222df17d1116fe91e871f9367;p=helm.git

support for generic reducibility ...
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
index e18b10a1a..d35fb52a2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
@@ -38,9 +38,9 @@ interpretation "uniform slicing (local environment)"
 interpretation "generic slicing (local environment)"
    'RDropStar b f L1 L2 = (drops b f L1 L2).
 
-definition d_liftable1: relation2 lenv term → predicate bool ≝
-                        λR,b. ∀f,L,K. ⬇*[b, f] L ≡ K →
-                        ∀T,U. ⬆*[f] T ≡ U → R K T → R L U.
+definition d_liftable1: predicate (relation2 lenv term) ≝
+                        λR. ∀K,T. R K T → ∀b,f,L. ⬇*[b, f] L ≡ K →
+                        ∀U. ⬆*[f] T ≡ U → R L U.
 
 definition d_liftable2: predicate (lenv → relation term) ≝
                         λR. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≡ K →
@@ -271,7 +271,7 @@ lemma drops_inv_pair2_isuni_next: ∀b,f,I,K,V,L1. 𝐔⦃f⦄ → ⬇*[b, ⫯f]
 [ #H elim (isid_inv_next … H) -H //
 | /2 width=5 by ex2_3_intro/
 ]
-qed-. 
+qed-.
 
 fact drops_inv_TF_aux: ∀f,L1,L2. ⬇*[Ⓕ, f] L1 ≡ L2 → 𝐔⦃f⦄ →
                        ∀I,K,V. L2 = K.ⓑ{I}V →
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_vector.ma
index 66bfbcfd6..d2c162806 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_vector.ma
@@ -17,15 +17,16 @@ include "basic_2/relocation/drops.ma".
 
 (* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************)
 
-definition d_liftable1_all: relation2 lenv term → predicate bool ≝
-                            λR,b. ∀f,L,K. ⬇*[b, f] L ≡ K →
-                            ∀Ts,Us. ⬆*[f] Ts ≡ Us →
-                            all … (R K) Ts → all … (R L) Us.
+definition d_liftable1_all: predicate (relation2 lenv term) ≝
+                            λR. ∀K,Ts. all … (R K) Ts →
+                            ∀b,f,L. ⬇*[b, f] L ≡ K →
+                            ∀Us. ⬆*[f] Ts ≡ Us → all … (R L) Us.
 
 (* Properties with generic relocation for term vectors **********************)
 
 (* Basic_2A1: was: d1_liftables_liftables_all *)
-lemma d1_liftable_liftable_all: ∀R,b. d_liftable1 R b → d_liftable1_all R b.
-#R #b #HR #f #L #K #HLK #Ts #Us #H elim H -Ts -Us normalize //
+lemma d1_liftable_liftable_all: ∀R. d_liftable1 R → d_liftable1_all R.
+#R #HR #K #Ts #HTs #b #f #L #HLK #Us #H
+generalize in match HTs; -HTs elim H -Ts -Us normalize //
 #Ts #Us #T #U #HTU #_ #IHTUs * /3 width=7 by conj/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
index 2d00bcbc2..f679a756d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
@@ -20,9 +20,9 @@ include "basic_2/relocation/lifts.ma".
 
 (* Basic_1: includes: lift_gen_lift *)
 (* Basic_2A1: includes: lift_div_le lift_div_be *)
-theorem lift_div4: ∀f2,Tf,T. ⬆*[f2] Tf ≡ T → ∀g2,Tg. ⬆*[g2] Tg ≡ T →
-                   ∀f1,g1. H_at_div f2 g2 f1 g1 →
-                   ∃∃T0. ⬆*[f1] T0 ≡ Tf & ⬆*[g1] T0 ≡ Tg.
+theorem lifts_div4: ∀f2,Tf,T. ⬆*[f2] Tf ≡ T → ∀g2,Tg. ⬆*[g2] Tg ≡ T →
+                    ∀f1,g1. H_at_div f2 g2 f1 g1 →
+                    ∃∃T0. ⬆*[f1] T0 ≡ Tf & ⬆*[g1] T0 ≡ Tg.
 #f2 #Tf #T #H elim H -f2 -Tf -T
 [ #f2 #s #g2 #Tg #H #f1 #g1 #_
   lapply (lifts_inv_sort2 … H) -H #H destruct
@@ -49,7 +49,7 @@ qed-.
 lemma lifts_div4_one: ∀f,Tf,T. ⬆*[↑f] Tf ≡ T →
                       ∀T1. ⬆*[1] T1 ≡ T →
                       ∃∃T0. ⬆*[1] T0 ≡ Tf & ⬆*[f] T0 ≡ T1.
-/4 width=6 by lift_div4, at_div_id_dx, at_div_pn/ qed-.
+/4 width=6 by lifts_div4, at_div_id_dx, at_div_pn/ qed-.
 
 theorem lifts_div3: ∀f2,T,T2. ⬆*[f2] T2 ≡ T → ∀f,T1. ⬆*[f] T1 ≡ T →
                     ∀f1. f2 ⊚ f1 ≡ f → ⬆*[f1] T1 ≡ T2.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
index 26d395f19..8acd0a571 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
@@ -122,4 +122,16 @@ lemma lifts_applv: ∀f:rtmap. ∀V1s,V2s. ⬆*[f] V1s ≡ V2s →
 #f #V1s #V2s #H elim H -V1s -V2s /3 width=1 by lifts_flat/
 qed.
 
+lemma liftsv_split_trans: ∀f,T1s,T2s. ⬆*[f] T1s ≡ T2s →
+                          ∀f1,f2. f2 ⊚ f1 ≡ f →
+                          ∃∃Ts. ⬆*[f1] T1s ≡ Ts & ⬆*[f2] Ts ≡ T2s.
+#f #T1s #T2s #H elim H -T1s -T2s
+[ /2 width=3 by liftsv_nil, ex2_intro/
+| #T1s #T2s #T1 #T2 #HT12 #_ #IH #f1 #f2 #Hf
+  elim (IH … Hf) -IH
+  elim (lifts_split_trans … HT12 … Hf) -HT12 -Hf
+  /3 width=5 by liftsv_cons, ex2_intro/
+]
+qed-.
+
 (* Basic_1: removed theorems 2: lifts1_nil lifts1_cons *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp.ma
index 12c661564..e0e3c54e9 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/syntax/genv.ma".
-include "basic_2/multiple/drops.ma".
+include "basic_2/relocation/drops_vector.ma".
 
 (* GENERIC COMPUTATION PROPERTIES *******************************************)
 
@@ -23,17 +23,20 @@ definition nf ≝ λRR:relation4 genv lenv term term. λRS:relation term.
 definition candidate: Type[0] ≝ relation3 genv lenv term.
 
 definition CP0 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
-                 ∀G. d_liftable1 (nf RR RS G) (Ⓕ).
+                 ∀G. d_liftable1 (nf RR RS G).
 
 definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
                  ∀G,L. ∃s. NF … (RR G L) RS (⋆s).
 
-definition CP2 ≝ λRP:candidate. ∀G. d_liftable1 (RP G) (Ⓕ).
+definition CP2 ≝ λRP:candidate. ∀G. d_liftable1 (RP G).
 
 definition CP3 ≝ λRP:candidate.
                  ∀G,L,T,s. RP G L (ⓐ⋆s.T) → RP G L T.
 
 (* requirements for generic computation properties *)
+(* Basic_1: includes: nf2_lift1 *)
+(* Basic_2A1: includes: gcp0_lifts *)
+(* Basic_2A1: includes: gcp2_lifts *)
 record gcp (RR:relation4 genv lenv term term) (RS:relation term) (RP:candidate) : Prop ≝
 { cp0: CP0 RR RS;
   cp1: CP1 RR RS;
@@ -43,16 +46,7 @@ record gcp (RR:relation4 genv lenv term term) (RS:relation term) (RP:candidate)
 
 (* Basic properties *********************************************************)
 
-(* Basic_1: was: nf2_lift1 *)
-lemma gcp0_lifts: ∀RR,RS,RP. gcp RR RS RP → ∀G. d_liftables1 (nf RR RS G) (Ⓕ).
-#RR #RS #RP #H #G @d1_liftable_liftables @(cp0 … H)
-qed.
-
-lemma gcp2_lifts: ∀RR,RS,RP. gcp RR RS RP → ∀G. d_liftables1 (RP G) (Ⓕ).
-#RR #RS #RP #H #G @d1_liftable_liftables @(cp2 … H)
-qed.
-
 (* Basic_1: was only: sns3_lifts1 *)
-lemma gcp2_lifts_all: ∀RR,RS,RP. gcp RR RS RP → ∀G. d_liftables1_all (RP G) (Ⓕ).
-#RR #RS #RP #H #G @d1_liftables_liftables_all /2 width=7 by gcp2_lifts/
-qed.
+(* Basic_2A1: was: gcp2_lifts_all *)
+lemma gcp2_all: ∀RR,RS,RP. gcp RR RS RP → ∀G. d_liftable1_all (RP G).
+/3 width=7 by cp2, d1_liftable_liftable_all/ qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_aaa.ma
index 925e111aa..111d967e5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_aaa.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_aaa.ma
@@ -12,11 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/multiple/lifts_lifts.ma".
-include "basic_2/multiple/drops_drops.ma".
-include "basic_2/static/aaa_lifts.ma".
 include "basic_2/static/aaa_aaa.ma".
-include "basic_2/computation/lsubc_drops.ma".
+include "basic_2/rt_computation/lsubc_drops.ma".
 
 (* GENERIC COMPUTATION PROPERTIES *******************************************)
 
@@ -25,69 +22,80 @@ include "basic_2/computation/lsubc_drops.ma".
 (* Basic_1: was: sc3_arity_csubc *)
 theorem acr_aaa_csubc_lifts: ∀RR,RS,RP.
                              gcp RR RS RP → gcr RR RS RP RP →
-                             ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,cs. ⬇*[Ⓕ, cs] L0 ≡ L1 →
-                             ∀T0. ⬆*[cs] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
+                             ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀b,f,L0. ⬇*[b, f] L0 ≡ L1 →
+                             ∀T0. ⬆*[f] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
                              ⦃G, L2, T0⦄ ϵ[RP] 〚A〛.
-#RR #RS #RP #H1RP #H2RP #G #L1 #T #A #H elim H -G -L1 -T -A
-[ #G #L #s #L0 #cs #HL0 #X #H #L2 #HL20
-  >(lifts_inv_sort1 … H) -H
+#RR #RS #RP #H1RP #H2RP #G #L1 #T @(fqup_wf_ind_eq … G L1 T) -G -L1 -T
+#Z #Y #X #IH #G #L1 * [ * | * [ #p ] * ]
+[ #s #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH
+  lapply (aaa_inv_sort … HA) -HA #H destruct
+  >(lifts_inv_sort1 … H0) -H0
   lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom
-  lapply (b4 … HAtom G L2 (◊)) /2 width=1 by/
-| #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #cs #HL01 #X #H #L2 #HL20
-  lapply (acr_gcr … H1RP H2RP B) #HB
-  elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct
-  lapply (drop_fwd_drop2 … HLK1) #HK1b
-  elim (drops_drop_trans … HL01 … HLK1) #X #cs1 #i0 #HL0 #H #Hi0 #Hcs1
-  >(at_mono … Hi1 … Hi0) -i1
-  elim (drops_inv_skip2 … Hcs1 … H) -cs1 #K0 #V0 #cs0 #Hcs0 #HK01 #HV10 #H destruct
-  elim (lsubc_drop_O1_trans … HL20 … HL0) -HL0 #X #HLK2 #H
+  lapply (s4 … HAtom G L2 (◊)) /2 width=1 by/
+| #i #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
+  elim (aaa_inv_lref_drops … HA) -HA #I #K1 #V1 #HLK1 #HKV1
+  elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct
+  lapply (acr_gcr … H1RP H2RP A) #HA
+  lapply (drops_trans … HL01 … HLK1 ??) -HL01 [3: |*: // ] #H
+  elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK0 #HY
+  lapply (drops_tls_at … Hf … HY) -Hf -HY #HY
+  elim (drops_inv_skip2 … HY) -HY #K0 #V0 #HK01 #HV10 #H destruct
+  elim (lifts_total V0 (𝐔❴⫯j❵)) #V #HV0
+  elim (lsubc_drops_trans_isuni … HL20 … HLK0) -HL20 -HLK0 // #Y #HLK2 #H
   elim (lsubc_inv_pair2 … H) -H *
   [ #K2 #HK20 #H destruct
-    elim (lift_total V0 0 (i0 +1)) #V #HV0
-    elim (lifts_lift_trans  … Hi0 … Hcs0 … HV10 … HV0) -HV10 #V2 #HV12 #HV2
-    lapply (b5 … HB ? G ? ? (◊) … HV0 HLK2) /3 width=7 by drops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *)
-  | -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hcs0
-    #K2 #V2 #A2 #HKV2A #H1KV0A #H2KV0A #_ #H1 #H2 destruct
-    lapply (drop_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
-    elim (lift_total V2 0 (i0 +1)) #V #HV2
-    lapply (b5 … HB ? G ? ? (◊) … (ⓝV3.V) … HLK2) /2 width=1 by lift_flat/
-    lapply (b7 … HB G L2 (◊)) /3 width=7 by gcr_lift/
+    lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
+    lapply (s5 … HA ? G ? ? (◊) … HV0 ?) -HA
+    /4 width=11 by acr_lifts, fqup_lref, drops_inv_gen/
+  | #K2 #V2 #B #HKV2 #HK2V0 #HKV0B #_ #H1 #H2 destruct -IH -HLK1
+    lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
+    lapply (aaa_lifts … HKV1 … HK01 … HV10) -HKV1 -HK01 -HV10 #HKV0A
+    lapply (aaa_mono … HKV0B … HKV0A) #H destruct -HKV0B -HKV0A
+    elim (lifts_total V2 (𝐔❴⫯j❵)) #V3 #HV23
+    lapply (s5 … HA … G … (◊) … (ⓝV0.V2) (ⓝV.V3) ????)
+    [3: |*: /2 width=9 by drops_inv_gen, lifts_flat/ ] -HLK2
+    lapply (s7 … HA G L2 (◊)) -HA /3 width=7 by acr_lifts/
   ]
-| #a #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #cs #HL0 #X #H #L2 #HL20
-  elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
+| #l #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH
+  elim (aaa_inv_gref … HA)
+| #V #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
+  elim (aaa_inv_abbr … HA) -HA #B #HV #HT
+  elim (lifts_inv_bind1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct
   lapply (acr_gcr … H1RP H2RP A) #HA
   lapply (acr_gcr … H1RP H2RP B) #HB
-  lapply (b1 … HB) -HB #HB
-  lapply (b6 … HA G L2 (◊) (◊)) /4 width=5 by lsubc_pair, drops_skip, liftv_nil/
-| #a #G #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #cs #HL0 #X #H #L2 #HL02
-  elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
-  @(acr_abst  … H1RP H2RP) /2 width=5 by/
-  #L3 #V3 #W3 #T3 #cs3 #HL32 #HW03 #HT03 #H1B #H2B
-  elim (drops_lsubc_trans … H1RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
-  lapply (aaa_lifts … L2 W3 … (cs @@ cs3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B
-  @(IHA (L2. ⓛW3) … (cs + 1 @@ cs3 + 1)) -IHA
-  /3 width=5 by lsubc_beta, drops_trans, drops_skip, lifts_trans/
-| #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #cs #HL0 #X #H #L2 #HL20
-  elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
-  /3 width=10 by drops_nil, lifts_nil/
-| #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #cs #HL0 #X #H #L2 #HL20
-  elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
+  lapply (s1 … HB) -HB #HB
+  lapply (s6 … HA G L2 (◊) (◊)) /4 width=10 by lsubc_pair, liftsv_nil, drops_skip/
+| #W #T #HG #HL #HT #Z0 #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
+  elim (aaa_inv_abst … HA) -HA #B #A #HW #HT #H destruct
+  elim (lifts_inv_bind1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct
+  @(acr_abst  … H1RP H2RP) /2 width=10 by/
+  #b3 #f3 #L3 #V3 #W3 #T3 #HL32 #HW03 #HT03 #H1B #H2B
+  elim (drops_lsubc_trans … H1RP … HL32 … HL20) -L2 #L2 #HL32 #HL20
+  lapply (aaa_lifts … HW … (f3∘f) L2 … W3 ?) -HW
+  [4: |*: /2 width=8 by drops_trans, lifts_trans/ ] #HW3
+  @(IH … ((↑f3)∘↑f) … (L2. ⓛW3)) -IH
+  /3 width=12 by lsubc_beta, drops_trans, drops_skip, lifts_trans/
+| #V #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
+  elim (aaa_inv_appl … HA) -HA #B #HV #HT
+  elim (lifts_inv_flat1 … H0) -H0 #V0 #T0 #HV0 #HT0 #H destruct
+  lapply (IH … HT … HL01 … HT0 … HL20) -HT -HT0
+  /3 width=10 by drops_refl, lifts_refl/
+| #W #T #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct
+  elim (aaa_inv_cast … HA) -HA #HW #HT
+  elim (lifts_inv_flat1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct
   lapply (acr_gcr … H1RP H2RP A) #HA
-  lapply (b7 … HA G L2 (◊)) /3 width=5 by/
+  lapply (s7 … HA G L2 (◊)) /3 width=10 by/
 ]
 qed.
 
 (* Basic_1: was: sc3_arity *)
 lemma acr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
                ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L, T⦄ ϵ[RP] 〚A〛.
-/2 width=8 by drops_nil, lifts_nil, acr_aaa_csubc_lifts/ qed.
+/3 width=9 by drops_refl, lifts_refl, acr_aaa_csubc_lifts/ qed.
 
 lemma gcr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
                ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → RP G L T.
 #RR #RS #RP #H1RP #H2RP #G #L #T #A #HT
 lapply (acr_gcr … H1RP H2RP A) #HA
-@(b1 … HA) /2 width=4 by acr_aaa/
+@(s1 … HA) /2 width=4 by acr_aaa/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma
index 3d1143900..6b5dfef44 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/gcp_cr.ma
@@ -14,10 +14,10 @@
 
 include "basic_2/notation/relations/ineint_5.ma".
 include "basic_2/syntax/aarity.ma".
-include "basic_2/multiple/mr2_mr2.ma".
-include "basic_2/multiple/lifts_lift_vector.ma".
-include "basic_2/multiple/drops_drop.ma".
-include "basic_2/computation/gcp.ma".
+include "basic_2/relocation/lifts_simple.ma".
+include "basic_2/relocation/lifts_lifts_vector.ma".
+include "basic_2/relocation/drops_drops.ma".
+include "basic_2/rt_computation/gcp.ma".
 
 (* GENERIC COMPUTATION PROPERTIES *******************************************)
 
@@ -39,11 +39,11 @@ definition S4 ≝ λRP,C:candidate.
                 ∀G,L,Vs. all … (RP G L) Vs → ∀s. C G L (ⒶVs.⋆s).
 
 definition S5 ≝ λC:candidate. ∀I,G,L,K,Vs,V1,V2,i.
-                C G L (ⒶVs.V2) → ⬆[0, i+1] V1 ≡ V2 →
-                ⬇[i] L ≡ K.ⓑ{I}V1 → C G L (ⒶVs.#i).
+                C G L (ⒶVs.V2) → ⬆*[⫯i] V1 ≡ V2 →
+                ⬇*[i] L ≡ K.ⓑ{I}V1 → C G L (ⒶVs.#i).
 
 definition S6 ≝ λRP,C:candidate.
-                ∀G,L,V1b,V2b. ⬆[0, 1] V1b ≡ V2b →
+                ∀G,L,V1b,V2b. ⬆*[1] V1b ≡ V2b →
                 ∀a,V,T. C G (L.ⓓV) (ⒶV2b.T) → RP G L V → C G L (ⒶV1b.ⓓ{a}V.T).
 
 definition S7 ≝ λC:candidate.
@@ -51,19 +51,19 @@ definition S7 ≝ λC:candidate.
 
 (* requirements for the generic reducibility candidate *)
 record gcr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:candidate) : Prop ≝
-{ b1: S1 RP C;
-  b2: S2 RR RS RP C;
-  b3: S3 C;
-  b4: S4 RP C;
-  b5: S5 C;
-  b6: S6 RP C;
-  b7: S7 C
+{ s1: S1 RP C;
+  s2: S2 RR RS RP C;
+  s3: S3 C;
+  s4: S4 RP C;
+  s5: S5 C;
+  s6: S6 RP C;
+  s7: S7 C
 }.
 
 (* the functional construction for candidates *)
 definition cfun: candidate → candidate → candidate ≝
-                 λC1,C2,G,K,T. ∀L,W,U,cs.
-                 ⬇*[Ⓕ, cs] L ≡ K → ⬆*[cs] T ≡ U → C1 G L W → C2 G L (ⓐW.U).
+                 λC1,C2,G,K,T. ∀f,L,W,U.
+                 ⬇*[Ⓕ, f] L ≡ K → ⬆*[f] T ≡ U → C1 G L W → C2 G L (ⓐW.U).
 
 (* the reducibility candidate associated to an atomic arity *)
 rec definition acr (RP:candidate) (A:aarity) on A: candidate ≝
@@ -73,21 +73,27 @@ match A with
 ].
 
 interpretation
-   "candidate of reducibility of an atomic arity (abstract)"
+   "reducibility candidate of an atomic arity (abstract)"
    'InEInt RP G L T A = (acr RP A G L T).
 
 (* Basic properties *********************************************************)
 
-(* Basic 1: was: sc3_lift *)
-lemma gcr_lift: ∀RR,RS,RP. gcp RR RS RP → ∀A,G. d_liftable1 (acr RP A G) (Ⓕ).
-#RR #RS #RP #H #A elim A -A
-/3 width=8 by cp2, drops_cons, lifts_cons/
-qed.
-
+(* Note: this requires multiple relocation *)
+(* Basic 1: includes: sc3_lift *)
+(* Basic 2A1: includes: gcr_lift *)
+(* Basic 2A1: note: gcr_lift should be acr_lift *)
 (* Basic_1: was: sc3_lift1 *)
-lemma gcr_lifts: ∀RR,RS,RP. gcp RR RS RP → ∀A,G. d_liftables1 (acr RP A G) (Ⓕ).
-#RR #RS #RP #H #A #G @d1_liftable_liftables /2 width=7 by gcr_lift/
-qed.
+(* Basic 2A1: was: gcr_lifts *)
+(* Basic 2A1: note: gcr_lifts should be acr_lifts *)
+lemma acr_lifts: ∀RR,RS,RP. gcp RR RS RP → ∀A,G. d_liftable1 (acr RP A G).
+#RR #RS #RP #H #A #G elim A -A
+[ /2 width=7 by cp2/
+| #B #A #HB #HA #K #T #HKT #b #f #L #HLK #U #HTU #f0 #L0 #W #U0 #HL0 #HU0 #HW
+  lapply (drops_trans … HL0 … HLK ??) [3:|*: // ] -L #HL0K
+  lapply (lifts_trans … HTU … HU0 ??) [3:|*: // ] -U #HTU0
+  /2 width=3 by/ (**) (* full auto fails *)
+]
+qed-.
 
 (* Basic_1: was:
    sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast
@@ -98,70 +104,70 @@ lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
 #B #A #IHB #IHA @mk_gcr
 [ #G #L #T #H
   elim (cp1 … H1RP G L) #s #HK
-  lapply (H L (⋆s) T (◊) ? ? ?) -H //
-  [ lapply (b2 … IHB G L (◊) … HK) //
-  | /3 width=6 by b1, cp3/
-  ]
-| #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #cs #HL0 #H #HB
-  elim (lifts_inv_applv1 … H) -H #V0b #T0 #HV0b #HT0 #H destruct
-  lapply (b1 … IHB … HB) #HV0
-  @(b2 … IHA … (V0 @ V0b))
-  /3 width=14 by gcp2_lifts_all, gcp2_lifts, gcp0_lifts, lifts_simple_dx, conj/
-| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #cs #HL0 #H #HB
-  elim (lifts_inv_applv1 … H) -H #V0b #Y #HV0b #HY #H destruct
+  lapply (s2 … IHB G L (◊) … HK) // #HB
+  lapply (H (𝐈𝐝) L (⋆s) T ? ? ?) -H
+  /3 width=6 by s1, cp3, drops_refl, lifts_refl/
+| #G #L #Vs #HVs #T #H1T #H2T #f #L0 #V0 #X #HL0 #H #HB
+  elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
+  lapply (s1 … IHB … HB) #HV0
+  @(s2 … IHA  … (V0@V0s)) /3 width=13 by cp0, gcp2_all, lifts_simple_dx, conj/
+| #p #G #L #Vs #U #T #W #HA #f #L0 #V0 #X #HL0 #H #HB
+  elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct
   elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
-  @(b3 … IHA … (V0 @ V0b)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/
-| #G #L #Vs #HVs #s #L0 #V0 #X #cs #HL0 #H #HB
-  elim (lifts_inv_applv1 … H) -H #V0b #Y #HV0b #HY #H destruct
+  @(s3 … IHA … (V0@V0s)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/
+| #G #L #Vs #HVs #s #f #L0 #V0 #X #HL0 #H #HB
+  elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   >(lifts_inv_sort1 … HY) -Y
-  lapply (b1 … IHB … HB) #HV0
-  @(b4 … IHA … (V0 @ V0b)) /3 width=7 by gcp2_lifts_all, conj/
-| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #cs #HL0 #H #HB
-  elim (lifts_inv_applv1 … H) -H #V0b #Y #HV0b #HY #H destruct
-  elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct
-  elim (drops_drop_trans … HL0 … HLK) #X #cs0 #i1 #HL02 #H #Hi1 #Hcs0
-  >(at_mono … Hi1 … Hi0) in HL02; -i1 #HL02
-  elim (drops_inv_skip2 … Hcs0 … H) -H -cs0 #L2 #W1 #cs0 #Hcs0 #HLK #HVW1 #H destruct
-  elim (lift_total W1 0 (i0 + 1)) #W2 #HW12
-  elim (lifts_lift_trans  … Hcs0 … HVW1 … HW12) // -Hcs0 -Hi0 #V3 #HV13 #HVW2
-  >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2
-  @(b5 … IHA … (V0 @ V0b) … HW12 HL02) /3 width=5 by lifts_applv/
-| #G #L #V1b #V2b #HV12b #a #V #T #HA #HV #L0 #V10 #X #cs #HL0 #H #HB
-  elim (lifts_inv_applv1 … H) -H #V10b #Y #HV10b #HY #H destruct
+  lapply (s1 … IHB … HB) #HV0
+  @(s4 … IHA … (V0@V0s)) /3 width=7 by gcp2_all, conj/
+| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #f #L0 #V0 #X #HL0 #H #HB
+  elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
+  elim (lifts_inv_lref1 … HY) -HY #j #Hf #H destruct
+  lapply (drops_trans … HL0 … HLK ??) [3: |*: // ] -HLK #H
+  elim (drops_split_trans … H) -H [ |*: /2 width=6 by after_uni_dx/ ] #Y #HLK0 #HY
+  lapply (drops_tls_at … Hf … HY) -HY #HY
+  elim (drops_inv_skip2 … HY) -HY #K0 #W1 #_ #HVW1 #H destruct
+  elim (lifts_total W1 (𝐔❴⫯j❵)) #W2 #HW12
+  lapply (lifts_trans … HVW1 … HW12 ??) -HVW1 [3: |*: // ] #H
+  lapply (lifts_conf … HV12 … H f ?) -V1 [ /2 width=3 by after_uni_succ_sn/ ] #HVW2
+  @(s5 … IHA … (V0@V0s) … HW12) /3 width=4 by drops_inv_gen, lifts_applv/
+| #G #L #V1s #V2s #HV12s #p #V #T #HA #HV #f #L0 #V10 #X #HL0 #H #HB
+  elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct
   elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct
-  elim (lift_total V10 0 1) #V20 #HV120
-  elim (liftv_total 0 1 V10b) #V20b #HV120b
-  @(b6 … IHA … (V10 @ V10b) (V20 @ V20b)) /3 width=7 by gcp2_lifts, liftv_cons/
-  @(HA … (cs + 1)) /2 width=2 by drops_skip/
+  elim (lifts_total V10 (𝐔❴1❵)) #V20 #HV120
+  elim (liftsv_total (𝐔❴1❵) V10s) #V20s #HV120s
+  @(s6 … IHA … (V10@V10s) (V20@V20s)) /3 width=7 by cp2, liftsv_cons/
+  @(HA … (↑f)) /2 width=2 by drops_skip/
   [ @lifts_applv //
-    elim (liftsv_liftv_trans_le … HV10b … HV120b) -V10b #V10b #HV10b #HV120b
-    >(liftv_mono … HV12b … HV10b) -V1b //
-  | @(gcr_lift … H1RP … HB … HV120) /2 width=2 by drop_drop/
+    lapply (liftsv_trans … HV10s … HV120s ??) -V10s [3: |*: // ] #H
+    elim (liftsv_split_trans … H (𝐔❴1❵) (↑f)) /2 width=1 by after_uni_one_sn/ #V10s #HV10s #HV120s
+    >(liftsv_mono … HV12s … HV10s) -V1s //
+  | @(acr_lifts … H1RP … HB … HV120) /3 width=2 by drops_refl, drops_drop/
   ]
-| #G #L #Vs #T #W #HA #HW #L0 #V0 #X #cs #HL0 #H #HB
-  elim (lifts_inv_applv1 … H) -H #V0b #Y #HV0b #HY #H destruct
+| #G #L #Vs #T #W #HA #HW #f #L0 #V0 #X #HL0 #H #HB
+  elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
   elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct
-  @(b7 … IHA … (V0 @ V0b)) /3 width=5 by lifts_applv/
+  @(s7 … IHA … (V0@V0s)) /3 width=5 by lifts_applv/
 ]
 qed.
 
 lemma acr_abst: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
-                ∀a,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → (
-                   ∀L0,V0,W0,T0,cs. ⬇*[Ⓕ, cs] L0 ≡ L → ⬆*[cs] W ≡ W0 → ⬆*[cs + 1] T ≡ T0 →
+                ∀p,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → (
+                   ∀b,f,L0,V0,W0,T0. ⬇*[b, f] L0 ≡ L → ⬆*[f] W ≡ W0 → ⬆*[↑f] T ≡ T0 →
                                    ⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛
                 ) →
-                ⦃G, L, ⓛ{a}W.T⦄ ϵ[RP] 〚②B.A〛.
-#RR #RS #RP #H1RP #H2RP #a #G #L #W #T #A #B #HW #HA #L0 #V0 #X #cs #HL0 #H #HB
+                ⦃G, L, ⓛ{p}W.T⦄ ϵ[RP] 〚②B.A〛.
+#RR #RS #RP #H1RP #H2RP #p #G #L #W #T #A #B #HW #HA #f #L0 #V0 #X #HL0 #H #HB
 lapply (acr_gcr … H1RP H2RP A) #HCA
 lapply (acr_gcr … H1RP H2RP B) #HCB
 elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
-lapply (gcr_lifts … H1RP … HL0 … HW0 HW) -HW #HW0
-lapply (b3 … HCA … a G L0 (◊)) #H @H -H
-lapply (b6 … HCA G L0 (◊) (◊) ?) // #H @H -H
+lapply (acr_lifts … H1RP … HW … HL0 … HW0) -HW #HW0
+lapply (s3 … HCA … p G L0 (◊)) #H @H -H
+lapply (s6 … HCA G L0 (◊) (◊) ?) // #H @H -H
 [ @(HA … HL0) //
-| lapply (b1 … HCB) -HCB #HCB
-  lapply (b7 … H2RP G L0 (◊)) /3 width=1 by/
+| lapply (s1 … HCB) -HCB #HCB
+  lapply (s7 … H2RP G L0 (◊)) /3 width=1 by/
 ]
 qed.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc.ma
index adc75dd3b..5b994b741 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc.ma
@@ -13,9 +13,8 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/lrsubeqc_4.ma".
-include "basic_2/static/lsubr.ma".
 include "basic_2/static/aaa.ma".
-include "basic_2/computation/gcp_cr.ma".
+include "basic_2/rt_computation/gcp_cr.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
 
@@ -96,12 +95,6 @@ lemma lsubc_inv_pair2: ∀RP,I,G,L1,K2,W. G ⊢ L1 ⫃[RP] K2.ⓑ{I} W →
                                  L1 = K1.ⓓⓝW.V & I = Abst.
 /2 width=3 by lsubc_inv_pair2_aux/ qed-.
 
-(* Basic forward lemmas *****************************************************)
-
-lemma lsubc_fwd_lsubr: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L1 ⫃ L2.
-#RP #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/
-qed-.
-
 (* Basic properties *********************************************************)
 
 (* Basic_1: was just: csubc_refl *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drop.ma
deleted file mode 100644
index 845a4dac0..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drop.ma
+++ /dev/null
@@ -1,70 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/static/aaa_lift.ma".
-include "basic_2/computation/lsubc.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
-
-(* Properties concerning basic local environment slicing ********************)
-
-(* Basic_1: was: csubc_drop_conf_O *)
-(* Note: the constant 0 can not be generalized *)
-lemma lsubc_drop_O1_trans: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → ∀K2,b,k. ⬇[b, 0, k] L2 ≡ K2 →
-                           ∃∃K1. ⬇[b, 0, k] L1 ≡ K1 & G ⊢ K1 ⫃[RP] K2.
-#RP #G #L1 #L2 #H elim H -L1 -L2
-[ #X #b #k #H elim (drop_inv_atom1 … H) -H /4 width=3 by drop_atom, ex2_intro/
-| #I #L1 #L2 #V #_ #IHL12 #X #b #k #H
-  elim (drop_inv_O1_pair1 … H) -H * #Hm #H destruct
-  [ elim (IHL12 L2 b 0) -IHL12 // #X #H <(drop_inv_O2 … H) -H
-    /3 width=3 by lsubc_pair, drop_pair, ex2_intro/
-  | elim (IHL12 … H) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
-  ]
-| #L1 #L2 #V #W #A #HV #H1W #H2W #_ #IHL12 #X #b #k #H
-  elim (drop_inv_O1_pair1 … H) -H * #Hm #H destruct
-  [ elim (IHL12 L2 b 0) -IHL12 // #X #H <(drop_inv_O2 … H) -H
-    /3 width=8 by lsubc_beta, drop_pair, ex2_intro/
-  | elim (IHL12 … H) -L2 /3 width=3 by drop_drop_lt, ex2_intro/
-  ]
-]
-qed-.
-
-(* Basic_1: was: csubc_drop_conf_rev *)
-lemma drop_lsubc_trans: ∀RR,RS,RP. gcp RR RS RP →
-                        ∀G,L1,K1,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 →
-                        ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⬇[Ⓕ, l, k] L2 ≡ K2.
-#RR #RS #RP #Hgcp #G #L1 #K1 #l #k #H elim H -L1 -K1 -l -k
-[ #l #k #Hm #X #H elim (lsubc_inv_atom1 … H) -H
-  >Hm /2 width=3 by ex2_intro/
-| #L1 #I #V1 #X #H
-  elim (lsubc_inv_pair1 … H) -H *
-  [ #K1 #HLK1 #H destruct /3 width=3 by lsubc_pair, drop_pair, ex2_intro/
-  | #K1 #V #W1 #A #HV1 #H1W1 #H2W1 #HLK1 #H1 #H2 #H3 destruct
-    /3 width=4 by lsubc_beta, drop_pair, ex2_intro/
-  ]
-| #I #L1 #K1 #V1 #k #_ #IHLK1 #K2 #HK12
-  elim (IHLK1 … HK12) -K1 /3 width=5 by lsubc_pair, drop_drop, ex2_intro/
-| #I #L1 #K1 #V1 #V2 #l #k #HLK1 #HV21 #IHLK1 #X #H
-  elim (lsubc_inv_pair1 … H) -H *
-  [ #K2 #HK12 #H destruct
-    elim (IHLK1 … HK12) -K1 /3 width=5 by lsubc_pair, drop_skip, ex2_intro/
-  | #K2 #V #W2 #A #HV2 #H1W2 #H2W2 #HK12 #H1 #H2 #H3 destruct
-    elim (lift_inv_flat1 … HV21) -HV21 #W3 #V3 #HW23 #HV3 #H destruct
-    elim (IHLK1 … HK12) #K #HL1K #HK2
-    lapply (gcr_lift … Hgcp … HV2 … HLK1 … HV3) -HV2
-    lapply (gcr_lift … Hgcp … H1W2 … HLK1 … HW23) -H1W2
-    /4 width=11 by lsubc_beta, aaa_lift, drop_skip, ex2_intro/
-  ]
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drops.ma
index 8fa9adfef..59ba61ad2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_drops.ma
@@ -12,20 +12,58 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/computation/lsubc_drop.ma".
+include "basic_2/static/aaa_drops.ma".
+include "basic_2/rt_computation/lsubc.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
 
-(* Properties concerning generic local environment slicing ******************)
+(* Properties with generic slicing ******************************************)
+
+(* Note: the premise 𝐔⦃f⦄ cannot be removed *)
+(* Basic_1: includes: csubc_drop_conf_O *)
+(* Basic_2A1: includes: lsubc_drop_O1_trans *)
+lemma lsubc_drops_trans_isuni: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 →
+                               ∀b,f,K2. 𝐔⦃f⦄ → ⬇*[b, f] L2 ≡ K2 →
+                               ∃∃K1. ⬇*[b, f] L1 ≡ K1 & G ⊢ K1 ⫃[RP] K2.
+#RP #G #L1 #L2 #H elim H -L1 -L2
+[ /2 width=3 by ex2_intro/
+| #I #L1 #L2 #V #HL12 #IH #b #f #K2 #Hf #H
+  elim (drops_inv_pair1_isuni … Hf H) -Hf -H *
+  [ #Hf #H destruct -IH
+    /3 width=3 by lsubc_pair, drops_refl, ex2_intro/
+  | #g #Hg #HLK2 #H destruct -HL12
+    elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
+  ]
+| #L1 #L2 #V #W #A #HV #H1W #H2W #HL12 #IH #b #f #K2 #Hf #H
+  elim (drops_inv_pair1_isuni … Hf H) -Hf -H *
+  [ #Hf #H destruct -IH
+    /3 width=8 by drops_refl, lsubc_beta, ex2_intro/
+  | #g #Hg #HLK2 #H destruct -HL12
+    elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
+  ]
+]
+qed-.
 
 (* Basic_1: was: csubc_drop1_conf_rev *)
+(* Basic_1: includes: csubc_drop_conf_rev *)
+(* Basic_2A1: includes: drop_lsubc_trans *)
 lemma drops_lsubc_trans: ∀RR,RS,RP. gcp RR RS RP →
-                         ∀G,L1,K1,cs. ⬇*[Ⓕ, cs] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 →
-                         ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⬇*[Ⓕ, cs] L2 ≡ K2.
-#RR #RS #RP #Hgcp #G #L1 #K1 #cs #H elim H -L1 -K1 -cs
-[ /2 width=3 by drops_nil, ex2_intro/
-| #L1 #L #K1 #cs #l #k #_ #HLK1 #IHL #K2 #HK12
-  elim (drop_lsubc_trans … Hgcp … HLK1 … HK12) -Hgcp -K1 #K #HLK #HK2
-  elim (IHL … HLK) -IHL -HLK /3 width=5 by drops_cons, ex2_intro/
+                         ∀b,f,G,L1,K1. ⬇*[b, f] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 →
+                         ∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⬇*[b, f] L2 ≡ K2.
+#RR #RS #RP #HR #b #f #G #L1 #K1 #H elim H -f -L1 -K1
+[ #f #Hf #Y #H lapply (lsubc_inv_atom1 … H) -H
+  #H destruct /4 width=3 by lsubc_atom, drops_atom, ex2_intro/
+| #f #I #L1 #K1 #V1 #_ #IH #K2 #HK12 elim (IH … HK12) -K1
+  /3 width=5 by lsubc_pair, drops_drop, ex2_intro/
+| #f #I #L1 #K1 #V1 #V2 #HLK1 #HV21 #IH #X #H elim (lsubc_inv_pair1 … H) -H *
+  [ #K2 #HK12 #H destruct -HLK1
+    elim (IH … HK12) -K1 /3 width=5 by lsubc_pair, drops_skip, ex2_intro/
+  | #K2 #V #W2 #A #HV #H1W2 #H2W2 #HK12 #H1 #H2 #H3 destruct
+    elim (lifts_inv_flat1 … HV21) -HV21 #W3 #V3 #HW23 #HV3 #H destruct
+    elim (IH … HK12) -IH -HK12 #K #HL1K #HK2
+    lapply (acr_lifts … HR … HV … HLK1 … HV3) -HV
+    lapply (acr_lifts … HR … H1W2 … HLK1 … HW23) -H1W2
+    /4 width=10 by lsubc_beta, aaa_lifts, drops_skip, ex2_intro/
+  ]
 ]
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsuba.ma
index 3a17f0e5b..2969b9a52 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsuba.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsuba.ma
@@ -13,11 +13,11 @@
 (**************************************************************************)
 
 include "basic_2/static/lsuba.ma".
-include "basic_2/computation/gcp_aaa.ma".
+include "basic_2/rt_computation/gcp_aaa.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
 
-(* properties concerning lenv refinement for atomic arity assignment ********)
+(* Properties with lenv refinement for atomic arity assignment **************)
 
 lemma lsuba_lsubc: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
                    ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → G ⊢ L1 ⫃[RP] L2.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsubr.ma
new file mode 100644
index 000000000..045ad95bd
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsubc_lsubr.ma
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/static/lsubr.ma".
+include "basic_2/rt_computation/lsubc.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
+
+(* Forward lemmas with restricted refinement for local environments *********)
+
+lemma lsubc_fwd_lsubr: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L1 ⫃ L2.
+#RP #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
index 41a6c9556..b47d0e449 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt
@@ -1 +1,3 @@
+lsubc.ma lsubc_drops.ma lsubc_lsubr.ma lsubc_lsuba.ma
+gcp.ma gcp_cr.ma gcp_aaa.ma
 cpxs.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_drops.ma
index abe54f1fb..13e7d528e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsuba_drops.ma
@@ -45,9 +45,9 @@ qed-.
 
 (* Note: the premise 𝐔⦃f⦄ cannot be removed *)
 (* Basic_2A1: includes: lsuba_drop_O1_trans *)
-lemma lsuba_drop_O1_trans: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 →
-                           ∀b,f,K2. 𝐔⦃f⦄ → ⬇*[b, f] L2 ≡ K2 →
-                           ∃∃K1. G ⊢ K1 ⫃⁝ K2 & ⬇*[b, f] L1 ≡ K1.
+lemma lsuba_drops_trans_isuni: ∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 →
+                               ∀b,f,K2. 𝐔⦃f⦄ → ⬇*[b, f] L2 ≡ K2 →
+                               ∃∃K1. G ⊢ K1 ⫃⁝ K2 & ⬇*[b, f] L1 ≡ K1.
 #G #L1 #L2 #H elim H -L1 -L2
 [ /2 width=3 by ex2_intro/
 | #I #L1 #L2 #V #HL12 #IH #b #f #K2 #Hf #H
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 bd2ddaa42..4d35bf981 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -124,16 +124,11 @@ table {
              [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ] 
           }
         ]
-(*
-        [ { "local env. ref. for generic reducibility" * } {
-             [ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drop" + "lsubc_drops" + "lsubc_lsuba" * ]
-          }
-        ]
-        [ { "support for generic computation properties" * } {
+        [ { "generic reducibility" * } {
+             [ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drop" + "lsubc_drops" + "lsubc_lsubr" + "lsubc_lsuba" * ]        
              [ "gcp" "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]
           }
-        ]
-*)        
+        ]        
      }
    ]
    class "water"