From f82a900182012664dd58eb1d8ab012c2a6f541ab Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 16 Jan 2017 11:24:12 +0000
Subject: [PATCH] advances towards confluence of reduction in local
 environments ...

---
 .../basic_2/relocation/lexs_lexs.ma           |   2 -
 .../basic_2/relocation/lreq_lreq.ma           |   1 -
 .../basic_2/rt_transition/lfpr_lfpr.ma        |   2 +-
 .../basic_2/rt_transition/lfpr_main.ma        |  21 +++
 .../basic_2/rt_transition/lfpx_frees.ma       |  39 +++--
 .../lambdadelta/basic_2/static/lfeq_lfeq.ma   |   1 -
 .../lambdadelta/basic_2/static/lfxs.ma        |  11 ++
 .../lambdadelta/basic_2/static/lfxs_lfxs.ma   |  23 +++
 .../lambdadelta/basic_2/static/lfxs_main.ma   |  50 ------
 .../lambdadelta/basic_2/static/lsubf.ma       | 153 ++++++------------
 .../lambdadelta/basic_2/static/lsubf_frees.ma |  50 +++---
 .../lambdadelta/basic_2/static/lsubr.ma       |  43 ++---
 .../lambdadelta/basic_2/web/basic_2_src.tbl   |  12 +-
 .../ground_2/relocation/rtmap_sle.ma          |  11 ++
 .../ground_2/relocation/rtmap_sor.ma          |   2 +
 15 files changed, 205 insertions(+), 216 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_main.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma
index cd7e64c51..c0d7c6a12 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma
@@ -13,8 +13,6 @@
 (**************************************************************************)
 
 include "ground_2/relocation/rtmap_sand.ma".
-include "ground_2/relocation/rtmap_sor.ma".
-include "basic_2/relocation/lexs.ma".
 include "basic_2/relocation/drops.ma".
 
 (* GENERIC ENTRYWISE EXTENSION OF CONTEXT-SENSITIVE REALTIONS FOR TERMS *****)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma
index c823270ec..42aaf3eea 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma
@@ -13,7 +13,6 @@
 (**************************************************************************)
 
 include "basic_2/relocation/lexs_lexs.ma".
-include "basic_2/relocation/lreq.ma".
 
 (* RANGED EQUIVALENCE FOR LOCAL ENVIRONMENTS ********************************)
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma
index a78a84a89..80310acaf 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma
@@ -298,7 +298,7 @@ lapply (lifts_mono … HX … HVU) -HX #H destruct
 /4 width=7 by cpm_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *)
 qed-.
 
-theorem cpr_conf_lfpr: ∀h,G. R_confluent_lfxs (cpm 0 h G) (cpm 0 h G) (cpm 0 h G) (cpm 0 h G).
+theorem cpr_conf_lfpr: ∀h,G. R_confluent2_lfxs (cpm 0 h G) (cpm 0 h G) (cpm 0 h G) (cpm 0 h G).
 #h #G #L0 #T0 @(fqup_wf_ind_eq … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [| * ]
 [ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct
   elim (cpr_inv_atom1_drops … H1) -H1
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_main.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_main.ma
new file mode 100644
index 000000000..de8e8a719
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_main.ma
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/lfxs_lfxs.ma".
+include "basic_2/rt_transition/lfpr_lfpr.ma".
+
+theorem lfpr_conf: ∀h,G,T. confluent … (lfpr h G T).
+#h #G @lfxs_conf [ | @cpr_conf_lfpr ]
+qed-.
+
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma
index 935109f90..7e184e1a4 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma
@@ -15,6 +15,8 @@
 include "basic_2/relocation/drops_lexs.ma".
 include "basic_2/s_computation/fqup_weight.ma".
 include "basic_2/static/frees_drops.ma".
+include "basic_2/static/lsubf_frees.ma".
+include "basic_2/static/lfxs.ma".
 include "basic_2/rt_transition/cpx_drops.ma".
 
 (* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
@@ -40,10 +42,10 @@ axiom frees_pair_flat: ∀L,T,f1,I1,V1. L.ⓑ{I1}V1 ⊢ 𝐅*⦃T⦄ ≡ f1 →
                        ∀I0,I. L.ⓑ{I0}ⓕ{I}V1.V2 ⊢ 𝐅*⦃T⦄ ≡ f0.
 
 (* Basic_2A1: was: lpx_cpx_frees_trans *)
-lemma cpx_frees_trans_lexs: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
-                            ∀L2. L1 ⦻*[cpx h G, cfull, f1] L2 →
-                            ∀T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 →
-                            ∃∃f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1.
+lemma cpx_frees_conf_lfpx: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
+                           ∀L2. L1 ⦻*[cpx h G, cfull, f1] L2 →
+                           ∀T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 →
+                           ∃∃f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1.
 #h #G #L1 #T1 @(fqup_wf_ind_eq … G L1 T1) -G -L1 -T1
 #G0 #L0 #U0 #IH #G #L1 * *
 [ -IH #s #HG #HL #HU #g1 #H1 #L2 #_ #U2 #H0 destruct
@@ -121,13 +123,26 @@ lemma cpx_frees_trans_lexs: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
     lapply (sle_lexs_trans … H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W
     lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T
     lapply (lexs_inv_tl … Abst … HL12T … HW12 ?) // -HL12T #HL12T
+    elim (sor_isfin_ex gV1 gW1) /2 width=3 by frees_fwd_isfin/ #g0 #Hg0 #_
+    lapply (sor_trans2 … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1
+    lapply (sor_sym … Hg0) -Hg0 #Hg0
     elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21
     elim (IH … HgW1 … HL12W … HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21
     elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21
+    elim (sor_isfin_ex gV2 (⫱gT2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #gVT2 #HgVT2 #_
+    elim (lsubf_frees_trans … HgT2 (⫯gVT2) … (L2.ⓓⓝW2.V2))
+    [2: /4 width=3 by lsubf_refl, lsubf_beta, sor_inv_sle_dx, sle_inv_tl_sn/ ] -HgT2
+    #gT0 #HgT0 #HgT20
     elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #gV0 #HgV0 #H
-    elim (sor_isfin_ex gV0 (⫱gT2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_
+    elim (sor_isfin_ex gV0 (⫱gT0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_
     @(ex2_intro … g2)
-    [ @(frees_bind … Hg2) /2 width=5 by frees_flat/ ]
+    [ @(frees_bind … Hg2) /2 width=5 by frees_flat/
+    | -L2 @(sor_inv_sle … Hg2) -Hg2
+      [ /3 width=11 by sor_inv_sle_sn_trans, monotonic_sle_sor/
+      | @sle_xn_tl [2:|*: // ] @(sle_trans … HgT20) -HgT20
+        /4 width=8 by monotonic_sle_sor, sor_inv_sle_dx_trans, sle_tl, sle_next/
+      ] (**) (* full auto too slow *)
+    ]
   | #p #V2 #V #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #H0 #H1 #H destruct
     elim (frees_inv_bind … HgT0) -HgT0 #gW1 #gT1 #HgW1 #HgT1 #HgT0
     lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V
@@ -149,10 +164,12 @@ lemma cpx_frees_trans_lexs: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 →
     /4 width=10 by frees_flat, frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/
   ]
 ]
+qed-.
 
-lemma cpx_frees_trans: ∀h,o,G. frees_trans (cpx h o G).
-/2 width=8 by lpx_cpx_frees_trans/ qed-.
+(* Basic_2A1: was: cpx_frees_trans *)
+lemma cpx_frees_conf: ∀h,G. R_frees_confluent (cpx h G).
+/3 width=7 by cpx_frees_conf_lfpx, lexs_refl/ qed-.
 
-lemma lpx_frees_trans: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 →
-                       ∀U,i. L2 ⊢ i ϵ 𝐅*[0]⦃U⦄ → L1 ⊢ i ϵ 𝐅*[0]⦃U⦄.
-/2 width=8 by lpx_cpx_frees_trans/ qed-.
+(* Basic_2A1: was: lpx_frees_trans *)
+lemma lfpx_frees_conf: ∀h,G. lexs_frees_confluent (cpx h G) cfull.
+/2 width=7 by cpx_frees_conf_lfpx/ qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma
index 602c58685..677f53973 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_lfeq.ma
@@ -13,7 +13,6 @@
 (**************************************************************************)
 
 include "basic_2/relocation/lreq_lreq.ma".
-include "basic_2/static/frees_frees.ma".
 include "basic_2/static/lfxs_lfxs.ma".
 include "basic_2/static/lfeq_lreq.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
index 605af05ce..2064f1217 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma
@@ -26,6 +26,17 @@ definition lfxs (R) (T): relation lenv ≝
 interpretation "generic extension on referred entries (local environment)"
    'RelationStar R T L1 L2 = (lfxs R T L1 L2).
 
+definition R_frees_confluent: predicate (relation3 lenv term term) ≝
+                              λRN.
+                              ∀f1,L,T1. L ⊢ 𝐅*⦃T1⦄ ≡ f1 → ∀T2. RN L T1 T2 →
+                              ∃∃f2. L ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1.
+
+definition lexs_frees_confluent: relation (relation3 lenv term term) ≝
+                                 λRN,RP.
+                                 ∀f1,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 →
+                                 ∀L2. L1 ⦻*[RN, RP, f1] L2 →
+                                 ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1.
+
 definition R_confluent2_lfxs: relation4 (relation3 lenv term term)
                                         (relation3 lenv term term) … ≝
                               λR1,R2,RP1,RP2.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma
index 5360aeddc..26289760b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma
@@ -13,6 +13,8 @@
 (**************************************************************************)
 
 include "basic_2/relocation/lexs_lexs.ma".
+include "basic_2/static/frees_fqup.ma".
+include "basic_2/static/frees_frees.ma".
 include "basic_2/static/lfxs.ma".
 
 (* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
@@ -33,3 +35,24 @@ theorem lfxs_flat: ∀R,I,L1,L2,V,T.
 #R #I #L1 #L2 #V #T * #f1 #HV #Hf1 * #f2 #HT #Hf2 elim (sor_isfin_ex f1 f2)
 /3 width=7 by frees_fwd_isfin, frees_flat, lexs_join, ex2_intro/
 qed.
+
+theorem lfxs_conf: ∀R. lexs_frees_confluent R cfull →
+                   R_confluent2_lfxs R R R R →
+                   ∀T. confluent … (lfxs R T).
+#R #H1R #H2R #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02
+lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12
+lapply (lexs_eq_repl_back … HL01 … Hf12) -f1 #HL01
+elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ]
+[ #L #HL1 #HL2
+  elim (H1R … Hf … HL01) -HL01 #f1 #Hf1 #H1
+  elim (H1R … Hf … HL02) -HL02 #f2 #Hf2 #H2
+  lapply (sle_lexs_trans … HL1 … H1) // -HL1 -H1 #HL1
+  lapply (sle_lexs_trans … HL2 … H2) // -HL2 -H2 #HL2
+  /3 width=5 by ex2_intro/
+| #g #I #K0 #V0 #n #HLK0 #Hgf #V1 #HV01 #V2 #HV02 #K1 #HK01 #K2 #HK02
+  elim (frees_drops_next … Hf … HLK0 … Hgf) -Hf -HLK0 -Hgf #g0 #Hg0 #H0
+  lapply (sle_lexs_trans … HK01 … H0) // -HK01 #HK01
+  lapply (sle_lexs_trans … HK02 … H0) // -HK02 #HK02
+  elim (H2R … HV01 … HV02 K1 … K2) /2 width=3 by ex2_intro/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma
deleted file mode 100644
index 444d413ef..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_main.ma
+++ /dev/null
@@ -1,50 +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/lfxs_lfxs.ma".
-include "basic_2/static/frees_fqup.ma".
-include "basic_2/static/frees_frees.ma".
-
-(* GENERIC EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ****)
-
-axiom frees_lexs_conf_sle: ∀RN,RP,f1,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 →
-                           ∀L2. L1 ⦻*[RN, RP, f1] L2 →
-                           ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1.
-
-theorem lfxs_conf: ∀R. R_confluent2_lfxs R R R R →
-                   ∀T. confluent … (lfxs R T).
-#R #H1R #T #L0 #L1 * #f1 #Hf1 #HL01 #L2 * #f #Hf #HL02
-lapply (frees_mono … Hf1 … Hf) -Hf1 #Hf12
-lapply (lexs_eq_repl_back … HL01 … Hf12) -f1 #HL01
-elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ]
-[ #L #HL1 #HL2
-  elim (frees_lexs_conf_sle … Hf … HL01) -HL01 #f1 #Hf1 #H1
-  elim (frees_lexs_conf_sle … Hf … HL02) -HL02 #f2 #Hf2 #H2
-  lapply (sle_lexs_trans … HL1 … H1) // -HL1 -H1 #HL1
-  lapply (sle_lexs_trans … HL2 … H2) // -HL2 -H2 #HL2
-  /3 width=5 by ex2_intro/
-| #g #I #K0 #V0 #n #HLK0 #Hgf #V1 #HV01 #V2 #HV02 #K1 #HK01 #K2 #HK02
-  elim (frees_drops_next … Hf … HLK0 … Hgf) -Hf -HLK0 -Hgf #g0 #Hg0 #H0
-  lapply (sle_lexs_trans … HK01 … H0) // -HK01 #HK01
-  lapply (sle_lexs_trans … HK02 … H0) // -HK02 #HK02
-  elim (H1R … HV01 … HV02 K1 … K2) /2 width=3 by ex2_intro/
-]
-qed-.
-
-(*
-lemma pippo: ∀R1,R2,RP1,RP2. R_confluent_lfxs R1 R2 RP1 RP2 →
-             lexs_confluent R1 R2 RP1 cfull RP2 cfull.
-#R1 #R2 #RP1 #RP2 #HR #f #L0 #T0 #T1 #HT01 #T2 #HT02 #L1 #HL01 #L2
-#HL02
-*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
index d5ad21f9d..3e6e63b07 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma
@@ -18,15 +18,11 @@ include "basic_2/static/frees.ma".
 (* RESTRICTED REFINEMENT FOR CONTEXT-SENSITIVE FREE VARIABLES ***************)
 
 inductive lsubf: relation4 lenv rtmap lenv rtmap ≝
-| lsubf_atom: ∀f. lsubf (⋆) f (⋆) f
-| lsubf_push: ∀f1,f2,I,L1,L2,V. lsubf L1 f1 L2 f2 →
-              lsubf (L1.ⓑ{I}V) (↑f1) (L2.ⓑ{I}V) (↑f2)
-| lsubf_next: ∀f1,f2,I,L1,L2,V. lsubf L1 f1 L2 f2 →
-              lsubf (L1.ⓑ{I}V) (⫯f1) (L2.ⓑ{I}V) (⫯f2)
-| lsubf_peta: ∀f1,f,f2,L1,L2,W,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f2 ⋓ f ≡ f1 →
-              lsubf L1 f1 L2 f2 → lsubf (L1.ⓓⓝW.V) (↑f1) (L2.ⓛW) (↑f2)
-| lsubf_neta: ∀f1,f,f2,L1,L2,W,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f2 ⋓ f ≡ f1 →
-              lsubf L1 f1 L2 f2 → lsubf (L1.ⓓⓝW.V) (⫯f1) (L2.ⓛW) (⫯f2)
+| lsubf_atom: ∀f1,f2. f2 ⊆ f1 → lsubf (⋆) f1 (⋆) f2
+| lsubf_pair: ∀f1,f2,I,L1,L2,V. lsubf L1 (⫱f1) L2 (⫱f2) → f2 ⊆ f1 →
+              lsubf (L1.ⓑ{I}V) f1 (L2.ⓑ{I}V) f2
+| lsubf_beta: ∀f,f1,f2,L1,L2,W,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f ⋓ ⫱f2 ≡ ⫱f1 → f2 ⊆ f1 →
+              lsubf L1 (⫱f1) L2 (⫱f2) → lsubf (L1.ⓓⓝW.V) f1 (L2.ⓛW) f2
 .
 
 interpretation
@@ -36,126 +32,77 @@ interpretation
 (* Basic inversion lemmas ***************************************************)
 
 fact lsubf_inv_atom1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L1 = ⋆ →
-                          L2 = ⋆ ∧ f1 = f2.
+                          L2 = ⋆ ∧ f2 ⊆ f1.
 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 [ /2 width=1 by conj/
-| #f1 #f2 #I #L1 #L2 #V #_ #H destruct
-| #f1 #f2 #I #L1 #L2 #V #_ #H destruct
-| #f1 #f #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
-| #f1 #f #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
+| #f1 #f2 #I #L1 #L2 #V #_ #_ #H destruct
+| #f #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H destruct
 ]
 qed-.
 
-lemma lsubf_inv_atom1: ∀f1,f2,L2. ⦃⋆, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                       L2 = ⋆ ∧ f1 = f2.
+lemma lsubf_inv_atom1: ∀f1,f2,L2. ⦃⋆, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L2 = ⋆ ∧ f2 ⊆ f1.
 /2 width=3 by lsubf_inv_atom1_aux/ qed-.
 
-fact lsubf_inv_push1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                          ∀g1,I,K1,X. f1 = ↑g1 → L1 = K1.ⓑ{I}X →
-                          (∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ↑g2 & L2 = K2.ⓑ{I}X) ∨
-                          ∃∃g,g2,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
-                                         ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abbr & f2 = ↑g2 & L2 = K2.ⓛW & X = ⓝW.V.
+fact lsubf_inv_pair1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                          ∀I,K1,X. L1 = K1.ⓑ{I}X →
+                          (∃∃K2. f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L2 = K2.ⓑ{I}X) ∨
+                          ∃∃f,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⋓ ⫱f2 ≡ ⫱f1 &
+                                      f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
-[ #f #g1 #J #K1 #X #_ #H destruct
-| #f1 #f2 #I #L1 #L2 #V #HL12 #g1 #J #K1 #X #H1 #H2 destruct
-  /3 width=5 by injective_push, ex3_2_intro, or_introl/
-| #f1 #f2 #I #L1 #L2 #V #_ #g1 #J #K1 #X #H elim (discr_next_push … H)
-| #f1 #f2 #f #L1 #L2 #W #V #Hf2 #Hf1 #HL12 #g1 #J #K1 #X #H1 #H2 destruct
-  /3 width=11 by injective_push, ex7_5_intro, or_intror/
-| #f1 #f2 #f #L1 #L2 #W #V #_ #_ #_ #g1 #J #K1 #X #H elim (discr_next_push … H)
+[ #f1 #f2 #_ #J #K1 #X #H destruct
+| #f1 #f2 #I #L1 #L2 #V #HL12 #H21 #J #K1 #X #H destruct
+  /3 width=3 by ex3_intro, or_introl/
+| #f #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H21 #HL12 #J #K1 #X #H destruct
+  /3 width=11 by ex7_4_intro, or_intror/
 ]
 qed-.
 
-lemma lsubf_inv_push1: ∀g1,f2,I,K1,L2,X. ⦃K1.ⓑ{I}X, ↑g1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                       (∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ↑g2 & L2 = K2.ⓑ{I}X) ∨
-                       ∃∃g,g2,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
-                                      ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abbr & f2 = ↑g2 & L2 = K2.ⓛW & X = ⓝW.V.
-/2 width=5 by lsubf_inv_push1_aux/ qed-.
-
-fact lsubf_inv_next1_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                          ∀g1,I,K1,X. f1 = ⫯g1 → L1 = K1.ⓑ{I}X →
-                          (∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ⫯g2 & L2 = K2.ⓑ{I}X) ∨
-                          ∃∃g,g2,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
-                                         ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abbr & f2 = ⫯g2 & L2 = K2.ⓛW & X = ⓝW.V.
-#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
-[ #f #g1 #J #K1 #X #_ #H destruct
-| #f1 #f2 #I #L1 #L2 #V #_ #g1 #J #K1 #X #H elim (discr_push_next … H)
-| #f1 #f2 #I #L1 #L2 #V #HL12 #g1 #J #K1 #X #H1 #H2 destruct
-  /3 width=5 by injective_next, ex3_2_intro, or_introl/
-| #f1 #f2 #f #L1 #L2 #W #V #_ #_ #_ #g1 #J #K1 #X #H elim (discr_push_next … H)
-| #f1 #f2 #f #L1 #L2 #W #V #Hf2 #Hf1 #HL12 #g1 #J #K1 #X #H1 #H2 destruct
-  /3 width=11 by injective_next, ex7_5_intro, or_intror/
-]
-qed-.
-
-lemma lsubf_inv_next1: ∀g1,f2,I,K1,L2,X. ⦃K1.ⓑ{I}X, ⫯g1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                       (∃∃g2,K2. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f2 = ⫯g2 & L2 = K2.ⓑ{I}X) ∨
-                       ∃∃g,g2,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
-                                      ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abbr & f2 = ⫯g2 & L2 = K2.ⓛW & X = ⓝW.V.
-/2 width=5 by lsubf_inv_next1_aux/ qed-.
+lemma lsubf_inv_pair1: ∀f1,f2,I,K1,L2,X. ⦃K1.ⓑ{I}X, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                       (∃∃K2. f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L2 = K2.ⓑ{I}X) ∨
+                       ∃∃f,K2,W,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⋓ ⫱f2 ≡ ⫱f1 &
+                                   f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abbr & L2 = K2.ⓛW & X = ⓝW.V.
+/2 width=3 by lsubf_inv_pair1_aux/ qed-.
 
 fact lsubf_inv_atom2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → L2 = ⋆ →
-                          L1 = ⋆ ∧ f1 = f2.
+                          L1 = ⋆ ∧ f2 ⊆ f1.
 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
 [ /2 width=1 by conj/
-| #f1 #f2 #I #L1 #L2 #V #_ #H destruct
-| #f1 #f2 #I #L1 #L2 #V #_ #H destruct
-| #f1 #f #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
-| #f1 #f #f2 #L1 #L2 #W #V #_ #_ #_ #H destruct
+| #f1 #f2 #I #L1 #L2 #V #_ #_ #H destruct
+| #f #f1 #f2 #L1 #L2 #W #V #_ #_ #_ #_ #H destruct
 ]
 qed-.
 
-lemma lsubf_inv_atom2: ∀f1,f2,L1. ⦃L1, f1⦄ ⫃𝐅* ⦃⋆, f2⦄ →
-                       L1 = ⋆ ∧ f1 = f2.
+lemma lsubf_inv_atom2: ∀f1,f2,L1. ⦃L1, f1⦄ ⫃𝐅* ⦃⋆, f2⦄ → L1 = ⋆ ∧ f2 ⊆ f1.
 /2 width=3 by lsubf_inv_atom2_aux/ qed-.
 
-fact lsubf_inv_push2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                          ∀g2,I,K2,W. f2 = ↑g2 → L2 = K2.ⓑ{I}W →
-                          (∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ↑g1 & L1 = K1.ⓑ{I}W) ∨
-                          ∃∃g,g1,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
-                                       ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abst & f1 = ↑g1 & L1 = K1.ⓓⓝW.V.
+fact lsubf_inv_pair2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                          ∀I,K2,W. L2 = K2.ⓑ{I}W →
+                          (∃∃K1.f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L1 = K1.ⓑ{I}W) ∨
+                          ∃∃f,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⋓ ⫱f2 ≡ ⫱f1 &
+                                    f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abst & L1 = K1.ⓓⓝW.V.
 #f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
-[ #f #g2 #J #K2 #X #_ #H destruct
-| #f1 #f2 #I #L1 #L2 #V #HL12 #g2 #J #K2 #X #H1 #H2 destruct
-  /3 width=5 by injective_push, ex3_2_intro, or_introl/
-| #f1 #f2 #I #L1 #L2 #V #_ #g2 #J #K2 #X #H elim (discr_next_push … H)
-| #f1 #f2 #f #L1 #L2 #W #V #Hf2 #Hf1 #HL12 #g2 #J #K2 #X #H1 #H2 destruct
-  /3 width=9 by injective_push, ex6_4_intro, or_intror/
-| #f1 #f2 #f #L1 #L2 #W #V #_ #_ #_ #g2 #J #K2 #X #H elim (discr_next_push … H)
+[ #f1 #f2 #_ #J #K2 #X #H destruct
+| #f1 #f2 #I #L1 #L2 #V #HL12 #H21 #J #K2 #X #H destruct
+  /3 width=3 by ex3_intro, or_introl/
+| #f #f1 #f2 #L1 #L2 #W #V #Hf #Hf1 #H21 #HL12 #J #K2 #X #H destruct
+  /3 width=7 by ex6_3_intro, or_intror/
 ]
 qed-.
 
-lemma lsubf_inv_push2: ∀f1,g2,I,L1,K2,W. ⦃L1, f1⦄ ⫃𝐅* ⦃K2.ⓑ{I}W, ↑g2⦄ →
-                       (∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ↑g1 & L1 = K1.ⓑ{I}W) ∨
-                       ∃∃g,g1,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
-                                    ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abst & f1 = ↑g1 & L1 = K1.ⓓⓝW.V.
-/2 width=5 by lsubf_inv_push2_aux/ qed-.
-
-fact lsubf_inv_next2_aux: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                          ∀g2,I,K2,W. f2 = ⫯g2 → L2 = K2.ⓑ{I}W →
-                          (∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ⫯g1 & L1 = K1.ⓑ{I}W) ∨
-                          ∃∃g,g1,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
-                                       ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abst & f1 = ⫯g1 & L1 = K1.ⓓⓝW.V.
-#f1 #f2 #L1 #L2 * -f1 -f2 -L1 -L2
-[ #f #g2 #J #K2 #X #_ #H destruct
-| #f1 #f2 #I #L1 #L2 #V #_ #g2 #J #K2 #X #H elim (discr_push_next … H)
-| #f1 #f2 #I #L1 #L2 #V #HL12 #g2 #J #K2 #X #H1 #H2 destruct
-  /3 width=5 by injective_next, ex3_2_intro, or_introl/
-| #f1 #f2 #f #L1 #L2 #W #V #_ #_ #_ #g2 #J #K2 #X #H elim (discr_push_next … H)
-| #f1 #f2 #f #L1 #L2 #W #V #Hf2 #Hf1 #HL12 #g2 #J #K2 #X #H1 #H2 destruct
-  /3 width=9 by injective_next, ex6_4_intro, or_intror/
-]
-qed-.
+lemma lsubf_inv_pair2: ∀f1,f2,I,L1,K2,W. ⦃L1, f1⦄ ⫃𝐅* ⦃K2.ⓑ{I}W, f2⦄ →
+                       (∃∃K1.f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & L1 = K1.ⓑ{I}W) ∨
+                       ∃∃f,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ f & f ⋓ ⫱f2 ≡ ⫱f1 &
+                                 f2 ⊆ f1 & ⦃K1, ⫱f1⦄ ⫃𝐅* ⦃K2, ⫱f2⦄ & I = Abst & L1 = K1.ⓓⓝW.V.
+/2 width=5 by lsubf_inv_pair2_aux/ qed-.
 
-lemma lsubf_inv_next2: ∀f1,g2,I,L1,K2,W. ⦃L1, f1⦄ ⫃𝐅* ⦃K2.ⓑ{I}W, ⫯g2⦄ →
-                       (∃∃g1,K1. ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & f1 = ⫯g1 & L1 = K1.ⓑ{I}W) ∨
-                       ∃∃g,g1,K1,V. K1 ⊢ 𝐅*⦃V⦄ ≡ g & g2 ⋓ g ≡ g1 &
-                                    ⦃K1, g1⦄ ⫃𝐅* ⦃K2, g2⦄ & I = Abst & f1 = ⫯g1 & L1 = K1.ⓓⓝW.V.
-/2 width=5 by lsubf_inv_next2_aux/ qed-.
+(* Basic forward lemmas *****************************************************)
+
+lemma lsubf_fwd_sle: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → f2 ⊆ f1.
+#f1 #f2 #L1 #L2 * //
+qed-.
 
 (* Basic properties *********************************************************)
 
-lemma lsubf_refl: bi_reflexive … lsubf.
-#L elim L -L //
-#L #I #V #IH #f elim (pn_split f) * /2 width=1 by lsubf_push, lsubf_next/
+lemma lsubf_refl: ∀L,f1,f2. f2 ⊆ f1 → ⦃L, f1⦄ ⫃𝐅* ⦃L, f2⦄.
+#L elim L -L /4 width=1 by lsubf_atom, lsubf_pair, sle_tl/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
index 65de4cfae..47fc2f75e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma
@@ -18,34 +18,34 @@ include "basic_2/static/lsubf.ma".
 
 (* Properties with context-sensitive free variables *************************)
 
-lemma lsubf_free_trans: ∀f2,L2,T. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 → ∀f,L1. ⦃L1, f⦄ ⫃𝐅* ⦃L2, f2⦄ →
-                        ∃∃f1. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 & f1 ⊆ f.
+axiom lsubf_frees_trans: ∀f2,L2,T. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 → ∀f,L1. ⦃L1, f⦄ ⫃𝐅* ⦃L2, f2⦄ →
+                         ∃∃f1. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 & f1 ⊆ f.
+(*
 #f2 #L2 #T #H elim H -f2 -L2 -T
 [ #f2 #I #Hf2 #f #L1 #H elim (lsubf_inv_atom2 … H) -H
-  #H1 #H2 destruct /3 width=3 by frees_atom, sle_refl, ex2_intro/
-| #f2 #I #K2 #W #s #_ #IH #f #L1 #H elim (lsubf_inv_push2 … H) -H *
-  [ #g1 #K1 #H12 #H1 #H2
-  | #g #g1 #K1 #V #Hg #Hg1 #H12 #H1 #H2 #H3
-  ] destruct elim (IH … H12) -f2 -K2
-  /3 width=7 by frees_sort, sle_push, ex2_intro/
-| #f2 #I #K2 #W #_ #IH #f #L1 #H elim (lsubf_inv_next2 … H) -H *
-  [ #g1 #K1 #H12 #H1 #H2 destruct elim (IH … H12) -f2 -K2
+  #H #_ destruct /3 width=3 by frees_atom, sle_isid_sn, ex2_intro/
+| #f2 #I #K2 #W #s #_ #IH #f #L1 #H elim (lsubf_inv_pair2 … H) -H *
+  [ #K1 #_ #H12 #H | #g #K1 #V #Hg #Hf #_ #H12 #H1 #H2 ]
+  destruct elim (IH … H12) -K2
+  /3 width=3 by frees_sort, sle_inv_tl_dx, ex2_intro/
+| #f2 #I #K2 #W #_ #IH #f #L1 #H elim (lsubf_inv_pair2 … H) -H *
+  [ #K1 #H elim (sle_inv_nx … H ??) -H [ <tl_next_rew |*: // ]
+    #g2 #_ #H1 #H12 #H2 destruct elim (IH … H12) -K2
     /3 width=7 by frees_zero, sle_next, ex2_intro/
-  | #g #g1 #K1 #V #Hg #Hg1 #H12 #H1 #H2 #H3 destruct
-    elim (IH … H12) -K2 #f1 #Hf1 #Hfg1
-    elim (sor_isfin_ex … f1 g ??)
-    /5 width=10 by frees_fwd_isfin, frees_flat, frees_zero, monotonic_sle_sor, sor_inv_sle_dx, sor_sle_sn, sle_next, ex2_intro/
+  | #g #K1 #V #Hg <tl_next_rew #Hf lapply (sor_sym … Hf) -Hf
+    #Hf #H elim (sle_inv_nx … H ??) -H [|*: // ]
+    #g2 #_ #H1 #H12 #H2 #H3 destruct elim (IH … H12) -K2
+    #f1 #Hf1 elim (sor_isfin_ex … f1 g ??)
+    /5 width=10 by frees_fwd_isfin, frees_flat, frees_zero, monotonic_sle_sor, sor_inv_sle_dx, sor_sym, sor_sle_sn, sle_next, ex2_intro/
   ]
-| #f2 #I #K2 #W #i #_ #IH #f #L1 #H elim (lsubf_inv_push2 … H) -H *
-  [ #g1 #K1 #H12 #H1 #H2
-  | #g #g1 #K1 #V #Hg #Hg1 #H12 #H1 #H2 #H3
-  ] destruct elim (IH … H12) -f2 -K2
-  /3 width=7 by frees_lref, sle_push, ex2_intro/
-| #f2 #I #K2 #W #l #_ #IH #f #L1 #H elim (lsubf_inv_push2 … H) -H *
-  [ #g1 #K1 #H12 #H1 #H2
-  | #g #g1 #K1 #V #Hg #Hg1 #H12 #H1 #H2 #H3
-  ] destruct elim (IH … H12) -f2 -K2
-  /3 width=7 by frees_gref, sle_push, ex2_intro/
+| #f2 #I #K2 #W #i #_ #IH #f #L1 #H elim (lsubf_inv_pair2 … H) -H *
+  [ #K1 #_ #H12 #H | #g #K1 #V #Hg #Hf #_ #H12 #H1 #H2 ]
+  destruct elim (IH … H12) -K2
+  /3 width=3 by frees_lref, sle_inv_tl_dx, ex2_intro/
+| #f2 #I #K2 #W #l #_ #IH #f #L1 #H elim (lsubf_inv_pair2 … H) -H *
+  [ #K1 #_ #H12 #H | #g #K1 #V #Hg #Hf #_ #H12 #H1 #H2 ]
+  destruct elim (IH … H12) -K2
+  /3 width=3 by frees_gref, sle_inv_tl_dx, ex2_intro/
 | #f2V #f2T #f2 #p #I #L2 #V #T #_ #_ #Hf2 #IHV #IHT #f #L1 #H12
 | #f2V #f2T #f2 #I #L2 #V #T #_ #_ #Hf2 #IHV #IHT #f #L1 #H12
- 
\ No newline at end of file
+*)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubr.ma
index c4ec6dd18..fe7ce2608 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubr.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubr.ma
@@ -58,39 +58,46 @@ lemma lsubr_inv_abst1: ∀K1,L2,W. K1.ⓛW ⫃ L2 →
                        L2 = ⋆ ∨ ∃∃K2. K1 ⫃ K2 & L2 = K2.ⓛW.
 /2 width=3 by lsubr_inv_abst1_aux/ qed-.
 
-fact lsubr_inv_abbr2_aux: ∀L1,L2. L1 ⫃ L2 → ∀K2,V. L2 = K2.ⓓV →
-                          ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓓV.
+fact lsubr_inv_pair2_aux: ∀L1,L2. L1 ⫃ L2 → ∀I,K2,W. L2 = K2.ⓑ{I}W →
+                          (∃∃K1. K1 ⫃ K2 & L1 = K1.ⓑ{I}W) ∨
+                          ∃∃K1,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V & I = Abst.
 #L1 #L2 * -L1 -L2
-[ #L #K2 #W #H destruct
-| #I #L1 #L2 #V #HL12 #K2 #W #H destruct /2 width=3 by ex2_intro/
-| #L1 #L2 #V1 #V2 #_ #K2 #W #H destruct
+[ #L #J #K2 #W #H destruct
+| #I #L1 #L2 #V #HL12 #J #K2 #W #H destruct /3 width=3 by ex2_intro, or_introl/
+| #L1 #L2 #V1 #V2 #HL12 #J #K2 #W #H destruct /3 width=4 by ex3_2_intro, or_intror/
 ]
 qed-.
 
+lemma lsubr_inv_pair2: ∀I,L1,K2,W. L1 ⫃ K2.ⓑ{I}W →
+                       (∃∃K1. K1 ⫃ K2 & L1 = K1.ⓑ{I}W) ∨
+                       ∃∃K1,V1. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V1 & I = Abst.
+/2 width=3 by lsubr_inv_pair2_aux/ qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
 lemma lsubr_inv_abbr2: ∀L1,K2,V. L1 ⫃ K2.ⓓV →
                        ∃∃K1. K1 ⫃ K2 & L1 = K1.ⓓV.
-/2 width=3 by lsubr_inv_abbr2_aux/ qed-.
-
-fact lsubr_inv_abst2_aux: ∀L1,L2. L1 ⫃ L2 → ∀K2,W. L2 = K2.ⓛW →
-                          (∃∃K1. K1 ⫃ K2 & L1 = K1.ⓛW) ∨
-                          ∃∃K1,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V.
-#L1 #L2 * -L1 -L2
-[ #L #K2 #W #H destruct
-| #I #L1 #L2 #V #HL12 #K2 #W #H destruct /3 width=3 by ex2_intro, or_introl/
-| #L1 #L2 #V1 #V2 #HL12 #K2 #W #H destruct /3 width=4 by ex2_2_intro, or_intror/
+#L1 #K2 #V #H elim (lsubr_inv_pair2 … H) -H *
+[ #K1 #HK12 #H destruct /2 width=3 by ex2_intro/
+| #K1 #V1 #_ #_ #H destruct
 ]
 qed-.
 
 lemma lsubr_inv_abst2: ∀L1,K2,W. L1 ⫃ K2.ⓛW →
                        (∃∃K1. K1 ⫃ K2 & L1 = K1.ⓛW) ∨
                        ∃∃K1,V. K1 ⫃ K2 & L1 = K1.ⓓⓝW.V.
-/2 width=3 by lsubr_inv_abst2_aux/ qed-.
+#L1 #K2 #W #H elim (lsubr_inv_pair2 … H) -H *
+[ #K1 #HK12 #H destruct /3 width=3 by ex2_intro, or_introl/
+| #K1 #V1 #HK12 #H #_ destruct /3 width=4 by ex2_2_intro, or_intror/
+]
+qed-.
 
 (* Basic forward lemmas *****************************************************)
 
 lemma lsubr_fwd_pair2: ∀I2,L1,K2,V2. L1 ⫃ K2.ⓑ{I2}V2 →
                        ∃∃I1,K1,V1. K1 ⫃ K2 & L1 = K1.ⓑ{I1}V1.
-* #L1 #K2 #V2 #H
-[ elim (lsubr_inv_abbr2 … H) | elim (lsubr_inv_abst2 … H) * ] -H
-/2 width=5 by ex2_3_intro/
+#I2 #L1 #K2 #V2 #H elim (lsubr_inv_pair2 … H) -H *
+[ #K1 #HK12 #H destruct /3 width=5 by ex2_3_intro/
+| #K1 #V1 #HK12 #H1 #H2 destruct /3 width=5 by ex2_3_intro/
+]
 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 c1be240bf..14974f02b 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
@@ -174,10 +174,6 @@ table {
              [ "aaa ( ⦃?,?⦄ ⊢ ? ⁝ ? )" "aaa_drops" + "aaa_fqus" + "aaa_lfeq" + "aaa_aaa" * ]
           }
         ]
-        [ { "restricted ref. for local env." * } {
-             [ "lsubr ( ? ⫃ ? )" "lsubr_length" + "lsubr_drops" + "lsubr_lsubr" * ]
-          }
-        ]
         [ { "equivalence for closures on referred entries" * } {
              [ "ffeq ( ⦃?,?,?⦄ ≡ ⦃?,?,?⦄ )" "ffeq_freq" * ]
           }
@@ -190,10 +186,18 @@ table {
              [ "lfxs ( ? ⦻*[?,?] ? )" "lfxs_length" + "lfxs_drops" + "lfxs_fqup" + "lfxs_lfxs" * ]
           }
         ]
+        [ { "restricted ref. for context-sensitive free variables" * } {
+             [ "lsubf ( ⦃?,?⦄ ⫃𝐅* ⦃?,?⦄ )" "lsubf_frees" * ]
+          }
+        ]        
         [ { "context-sensitive free variables" * } {
              [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_lreq" + "frees_drops" + "frees_fqup" + "frees_fqus" + "frees_frees" * ]
           }
         ]
+        [ { "restricted ref. for local env." * } {
+             [ "lsubr ( ? ⫃ ? )" "lsubr_length" + "lsubr_drops" + "lsubr_lsubr" * ]
+          }
+        ]
      }
    ]
    class "grass"
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma
index 2fc90abd1..c5d9428a5 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sle.ma
@@ -79,6 +79,13 @@ lemma sle_inv_px: ∀g1,g2. g1 ⊆ g2 → ∀f1. ↑f1 = g1 →
 /3 width=3 by ex2_intro, or_introl, or_intror/
 qed-.
 
+lemma sle_inv_xn: ∀g1,g2. g1 ⊆ g2 → ∀f2. ⫯f2 = g2 →
+                  (∃∃f1. f1 ⊆ f2 & ↑f1 = g1) ∨ ∃∃f1. f1 ⊆ f2 & ⫯f1 = g1.
+#g1 #g2 elim (pn_split g1) * #f1 #H1 #H #f2 #H2
+[ lapply (sle_inv_pn … H … H1 H2) | lapply (sle_inv_nn … H … H1 H2) ] -H -H2
+/3 width=3 by ex2_intro, or_introl, or_intror/
+qed-.
+
 (* Main properties **********************************************************)
 
 corec theorem sle_trans: Transitive … sle.
@@ -100,6 +107,10 @@ lemma sle_px_tl: ∀g1,g2. g1 ⊆ g2 → ∀f1. ↑f1 = g1 → f1 ⊆ ⫱g2.
 #g1 #g2 #H #f1 #H1 elim (sle_inv_px … H … H1) -H -H1 * //
 qed.
 
+lemma sle_xn_tl: ∀g1,g2. g1 ⊆ g2 → ∀f2. ⫯f2 = g2 → ⫱g1 ⊆ f2.
+#g1 #g2 #H #f2 #H2 elim (sle_inv_xn … H … H2) -H -H2 * //
+qed.
+
 lemma sle_tl: ∀f1,f2. f1 ⊆ f2 → ⫱f1 ⊆ ⫱f2.
 #f1 elim (pn_split f1) * #g1 #H1 #f2 #H
 [ lapply (sle_px_tl … H … H1) -H //
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
index 2a616742c..efa6b54d9 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
@@ -438,6 +438,8 @@ lemma sor_inv_sle_sn_trans: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. g ⊆ f1 → g
 lemma sor_inv_sle_dx_trans: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. g ⊆ f2 → g ⊆ f.
 /3 width=4 by sor_inv_sle_dx, sle_trans/ qed-.
 
+axiom sor_inv_sle: ∀f1,f2,f. f1 ⋓ f2 ≡ f → ∀g. f1 ⊆ g → f2 ⊆ g → f ⊆ g.
+
 (* Properties with inclusion ************************************************)
 
 corec lemma sor_sle_dx: ∀f1,f2. f1 ⊆ f2 → f1 ⋓ f2 ≡ f2.
-- 
2.39.2