From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 31 May 2016 19:06:53 +0000 (+0000)
Subject: frees_drops, initial versrion
X-Git-Tag: make_still_working~572
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=d64b4238ec803353f0a06f2aad25c173852b0526

frees_drops, initial versrion
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
index 324660cbf..8d22bcf00 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
@@ -69,6 +69,10 @@ definition dedropable_sn: predicate (rtmap → relation lenv) ≝
 
 (* Basic properties *********************************************************)
 
+lemma drops_atom_F: ∀f. ⬇*[Ⓕ, f] ⋆ ≡ ⋆.
+#f @drops_atom #H destruct
+qed.
+
 lemma drops_eq_repl_back: ∀b,L1,L2. eq_repl_back … (λf. ⬇*[b, f] L1 ≡ L2).
 #b #L1 #L2 #f1 #H elim H -f1 -L1 -L2
 [ /4 width=3 by drops_atom, isid_eq_repl_back/
@@ -168,7 +172,7 @@ fact drops_fwd_drop2_aux: ∀b,f2,X,Y. ⬇*[b, f2] X ≡ Y → ∀I,K,V. Y = K.
 | #f2 #I #L1 #L2 #V #_ #IHL #J #K #W #H elim (IHL … H) -IHL
   /3 width=7 by after_next, ex3_2_intro, drops_drop/
 | #f2 #I #L1 #L2 #V1 #V2 #HL #_ #_ #J #K #W #H destruct
-  lapply (isid_after_dx 𝐈𝐝 … f2) /3 width=9 by after_push, ex3_2_intro, drops_drop/
+  lapply (after_isid_dx 𝐈𝐝 … f2) /3 width=9 by after_push, ex3_2_intro, drops_drop/
 ]
 qed-.
 
@@ -343,7 +347,16 @@ lemma drops_inv_succ: ∀l,L1,L2. ⬇*[⫯l] L1 ≡ L2 →
 [ #H elim (isid_inv_next … H) -H //
 | /2 width=5 by ex2_3_intro/
 ]
-qed-. 
+qed-.
+
+(* Properties with uniform relocations **************************************)
+
+lemma drops_uni_ex: ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ ∨ ∃∃I,K,V. ⬇*[i] L ≡ K.ⓑ{I}V.
+#L elim L -L /2 width=1 by or_introl/
+#L #I #V #IH * /4 width=4 by drops_refl, ex1_3_intro, or_intror/
+#i elim (IH i) -IH /3 width=1 by drops_drop, or_introl/
+* /4 width=4 by drops_drop, ex1_3_intro, or_intror/
+qed-.  
 
 (* Basic_2A1: removed theorems 12:
               drops_inv_nil drops_inv_cons d1_liftable_liftables
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma
index 0b3279de9..e8dcdee40 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma
@@ -87,7 +87,7 @@ qed-.
 (* Basic_2A1: includes: drop_mono *)
 lemma drops_mono: ∀b1,f,L,L1. ⬇*[b1, f] L ≡ L1 →
                   ∀b2,L2. ⬇*[b2, f] L ≡ L2 → L1 = L2.
-#b1 #f #L #L1 lapply (isid_after_dx 𝐈𝐝 … f)
+#b1 #f #L #L1 lapply (after_isid_dx 𝐈𝐝 … f)
 /3 width=8 by drops_conf, drops_fwd_isid/
 qed-.
 
@@ -125,3 +125,9 @@ lapply (drops_eq_repl_back … Hf1 … H12) -Hf1 #H0
 lapply (drops_mono … H0 … Hf2) -L #H
 destruct /2 width=1 by and3_intro/
 qed-.
+
+lemma drops_inv_uni: ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ → ∀I,K,V. ⬇*[i] L ≡ K.ⓑ{I}V → ⊥.
+#L #i #H1 #I #K #V #H2
+lapply (drops_F … H2) -H2 #H2
+lapply (drops_mono … H2 … H1) -L -i #H destruct
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
index 495d5e45f..a621b819f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
@@ -249,6 +249,14 @@ qed-.
 
 (* Basic forward lemmas *****************************************************)
 
+lemma lifts_fwd_atom2: ∀f,I,X. ⬆*[f] X ≡ ⓪{I} → ∃J. X = ⓪{J}. 
+#f * #n #X #H
+[ lapply (lifts_inv_sort2 … H)
+| elim (lifts_inv_lref2 … H)
+| lapply (lifts_inv_gref2 … H)
+] -H /2 width=2 by ex_intro/
+qed-.
+
 (* Basic_2A1: includes: lift_inv_O2 *)
 lemma lifts_fwd_isid: ∀f,T1,T2. ⬆*[f] T1 ≡ T2 → 𝐈⦃f⦄ → T1 = T2.
 #f #T1 #T2 #H elim H -f -T1 -T2
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 8477714f3..2d00bcbc2 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
@@ -107,12 +107,12 @@ qed-.
 
 (* Basic_2A1: includes: lift_inj *)
 lemma lifts_inj: ∀f,T1,U. ⬆*[f] T1 ≡ U → ∀T2. ⬆*[f] T2 ≡ U → T1 = T2.
-#f #T1 #U #H1 #T2 #H2 lapply (isid_after_dx 𝐈𝐝  … f)
+#f #T1 #U #H1 #T2 #H2 lapply (after_isid_dx 𝐈𝐝  … f)
 /3 width=6 by lifts_div3, lifts_fwd_isid/
 qed-.
 
 (* Basic_2A1: includes: lift_mono *)
 lemma lifts_mono: ∀f,T,U1. ⬆*[f] T ≡ U1 → ∀U2. ⬆*[f] T ≡ U2 → U1 = U2.
-#f #T #U1 #H1 #U2 #H2 lapply (isid_after_sn 𝐈𝐝  … f)
+#f #T #U1 #H1 #U2 #H2 lapply (after_isid_sn 𝐈𝐝  … f)
 /3 width=6 by lifts_conf, lifts_fwd_isid/
 qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma
new file mode 100644
index 000000000..258d0c81b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/substitution/lpx_sn_drop.ma".
+include "basic_2/rt_transition/cpx_drops.ma".
+include "basic_2/rt_transition/lfpx.ma".
+
+(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+
+(* Properties on local environment slicing ***********************************)
+
+lemma lpx_drop_conf: ∀h,o,G. dropable_sn (lpx h o G).
+/3 width=6 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-.
+
+lemma drop_lpx_trans: ∀h,o,G. dedropable_sn (lpx h o G).
+/3 width=10 by lpx_sn_liftable_dedropable, cpx_lift/ qed-.
+
+lemma lpx_drop_trans_O1: ∀h,o,G. dropable_dx (lpx h o G).
+/2 width=3 by lpx_sn_dropable/ 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
new file mode 100644
index 000000000..d9f6445a0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma
@@ -0,0 +1,105 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/multiple/frees_lreq.ma".
+include "basic_2/multiple/frees_lift.ma".
+*)
+include "basic_2/s_computation/fqup_weight.ma".
+include "basic_2/rt_transition/cpx_drops.ma".
+include "basic_2/rt_transition/lfpx.ma".
+
+(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****)
+
+(* Properties with context-sensitive free variables ***************************)
+
+lemma lpx_cpx_frees_fwd_sge: ∀h,G,L1,U1,U2. ⦃G, L1⦄ ⊢ U1 ⬈[h] U2 →
+                             ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, U1] L2 →
+                             ∀g1. L1 ⊢ 𝐅*⦃U1⦄ ≡ g1 → ∀g2. L2 ⊢ 𝐅*⦃U2⦄ ≡ g2 →
+                             g2 ⊆ g1.
+#h #G #L1 #U1 @(fqup_wf_ind_eq … G L1 U1) -G -L1 -U1
+#G0 #L0 #U0 #IH #G #L1 * *
+[ #s #HG #HL #HU #U2 #H0 #L2 #_ #g1 #H1 #g2 #H2 -IH -G0 -L0 -U0
+  elim (cpx_inv_sort1 … H0) -H0 #H destruct
+  /3 width=3 by frees_inv_sort, sle_isid_sn/
+| #i #HG #HL #HU #U2 #H0 #L2 #HL12 #g1 #H1 #g2 #H2 destruct
+  elim (cpx_inv_lref1_drops … H0) -H0
+  [ #H destruct
+    lapply (frees_inv_lref … H1) -H1 #Hg1
+    lapply (frees_inv_sort … H2) -H2 #Hg2 /2 width=1 by sle_isid_sn/  
+
+
+
+| #l #HG #HL #HU #U2 #H0 #L2 #_ #g1 #H1 #g2 #H2 -IH -G0 -L0 -U0
+  lapply (cpx_inv_gref1 … H0) -H0 #H destruct
+  /3 width=3 by frees_inv_gref, sle_isid_sn/
+  
+| #j #HG #HL #HU #U2 #H1 #L2 #HL12 #i #H2 elim (cpx_inv_lref1 … H1) -H1
+  [ #H destruct elim (frees_inv_lref … H2) -H2 //
+    * #I #K2 #W2 #Hj #Hji #HLK2 #HW2
+    elim (lpx_drop_trans_O1 … HL12 … HLK2) -HL12 #Y #HLK1 #H
+    elim (lpx_inv_pair2 … H) -H #K1 #W1 #HK12 #HW12 #H destruct
+    /4 width=11 by frees_lref_be, fqup_lref/
+  | * #I #K1 #W1 #W0 #HLK1 #HW10 #HW0U2
+    lapply (drop_fwd_drop2 … HLK1) #H0
+    elim (lpx_drop_conf … H0 … HL12) -H0 -HL12 #K2 #HK12 #HLK2
+    elim (ylt_split i (j+1)) >yplus_SO2 #Hji
+    [ -IH elim (frees_inv_lift_be … H2 … HLK2 … HW0U2) /2 width=1 by ylt_fwd_succ2/
+    | lapply (frees_inv_lift_ge … H2 … HLK2 … HW0U2 ?) -L2 -U2 // destruct
+      /4 width=11 by frees_lref_be, fqup_lref, yle_succ1_inj/
+    ]
+  ]
+| -IH #p #HG #HL #HU #U2 #H1 >(cpx_inv_gref1 … H1) -H1 destruct
+   #L2 #_ #i #H2 elim (frees_inv_gref … H2)
+| #a #I #W1 #U1 #HG #HL #HU #X #HX #L2 #HL12 #i #Hi destruct
+  elim (cpx_inv_bind1 … HX) -HX *
+  [ #W2 #U2 #HW12 #HU12 #H destruct
+    elim (frees_inv_bind_O … Hi) -Hi
+    /4 width=7 by frees_bind_dx_O, frees_bind_sn, lpx_pair/
+  | #U2 #HU12 #HXU2 #H1 #H2 destruct
+    lapply (frees_lift_ge … Hi (L2.ⓓW1) (Ⓕ) … HXU2 ?)
+    /4 width=7 by frees_bind_dx_O, lpx_pair, drop_drop/
+  ]
+| #I #W1 #X1 #HG #HL #HU #X2 #HX2 #L2 #HL12 #i #Hi destruct
+  elim (cpx_inv_flat1 … HX2) -HX2 *
+  [ #W2 #U2 #HW12 #HU12 #H destruct
+    elim (frees_inv_flat … Hi) -Hi /3 width=7 by frees_flat_dx, frees_flat_sn/
+  | #HU12 #H destruct /3 width=7 by frees_flat_dx/
+  | #HW12 #H destruct /3 width=7 by frees_flat_sn/
+  | #b #W2 #V1 #V2 #U1 #U2 #HW12 #HV12 #HU12 #H1 #H2 #H3 destruct
+    elim (frees_inv_bind … Hi) -Hi #Hi
+    [ elim (frees_inv_flat … Hi) -Hi
+      /4 width=7 by frees_flat_dx, frees_flat_sn, frees_bind_sn/
+    | lapply (lreq_frees_trans … Hi (L2.ⓛV2) ?) /2 width=1 by lreq_succ/ -Hi #HU2
+      lapply (frees_weak … HU2 0 ?) -HU2
+      /5 width=7 by frees_bind_dx_O, frees_flat_dx, lpx_pair/
+    ]
+  | #b #W2 #W0 #V1 #V2 #U1 #U2 #HW12 #HW20 #HV12 #HU12 #H1 #H2 #H3 destruct
+    elim (frees_inv_bind_O … Hi) -Hi #Hi
+    [ /4 width=7 by frees_flat_dx, frees_bind_sn/
+    | elim (frees_inv_flat … Hi) -Hi
+      [ #HW0 lapply (frees_inv_lift_ge … HW0 L2 (Ⓕ) … HW20 ?) -W0
+        /3 width=7 by frees_flat_sn, drop_drop/
+      | /5 width=7 by frees_bind_dx_O, frees_flat_dx, lpx_pair/
+      ]
+    ]
+  ]
+]
+qed-.
+
+lemma cpx_frees_trans: ∀h,o,G. frees_trans (cpx h o G).
+/2 width=8 by lpx_cpx_frees_trans/ 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-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_drop.ma
deleted file mode 100644
index 6473e73c0..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_drop.ma
+++ /dev/null
@@ -1,78 +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/substitution/lpx_sn_drop.ma".
-include "basic_2/reduction/cpx_lift.ma".
-include "basic_2/reduction/lpx.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-(* Properties on local environment slicing ***********************************)
-
-lemma lpx_drop_conf: ∀h,o,G. dropable_sn (lpx h o G).
-/3 width=6 by lpx_sn_deliftable_dropable, cpx_inv_lift1/ qed-.
-
-lemma drop_lpx_trans: ∀h,o,G. dedropable_sn (lpx h o G).
-/3 width=10 by lpx_sn_liftable_dedropable, cpx_lift/ qed-.
-
-lemma lpx_drop_trans_O1: ∀h,o,G. dropable_dx (lpx h o G).
-/2 width=3 by lpx_sn_dropable/ qed-.
-
-(* Properties on supclosure *************************************************)
-
-lemma fqu_lpx_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
-                     ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, o] K2 →
-                     ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, o] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, o] T & ⦃G1, K1, T⦄ ⊐ ⦃G2, K2, T2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpx_pair, ex3_2_intro/
-[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpx_inv_pair1 … H) -H
-  #K2 #W2 #HLK2 #HVW2 #H destruct
-  /3 width=5 by cpx_pair_sn, fqu_bind_dx, ex3_2_intro/
-| #G #L1 #K1 #T1 #U1 #k #HLK1 #HTU1 #K2 #HK12
-  elim (drop_lpx_trans … HLK1 … HK12) -HK12
-  /3 width=7 by fqu_drop, ex3_2_intro/
-]
-qed-.
-
-lemma fquq_lpx_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
-                      ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, o] K2 →
-                      ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, o] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h, o] T & ⦃G1, K1, T⦄ ⊐⸮ ⦃G2, K2, T2⦄.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H
-[ #HT12 elim (fqu_lpx_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/
-| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-lemma lpx_fqu_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
-                     ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 →
-                     ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, o] T & ⦃G1, K1, T⦄ ⊐ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
-/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, drop_drop, ex3_2_intro/
-| #G #L1 #K1 #T1 #U1 #k #HLK1 #HTU1 #L0 #HL01
-  elim (lpx_drop_trans_O1 … HL01 … HLK1) -L1
-  /3 width=5 by fqu_drop, ex3_2_intro/
-]
-qed-.
-
-lemma lpx_fquq_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
-                      ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, o] L1 →
-                      ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡[h, o] T & ⦃G1, K1, T⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, o] L2.
-#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #HKL1 elim (fquq_inv_gen … H) -H
-[ #HT12 elim (lpx_fqu_trans … HT12 … HKL1) /3 width=5 by fqu_fquq, ex3_2_intro/
-| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_frees.ma
deleted file mode 100644
index fa314630d..000000000
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpx_frees.ma
+++ /dev/null
@@ -1,88 +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/multiple/frees_lreq.ma".
-include "basic_2/multiple/frees_lift.ma".
-include "basic_2/reduction/lpx_drop.ma".
-
-(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************)
-
-(* Properties on context-sensitive free variables ***************************)
-
-lemma lpx_cpx_frees_trans: ∀h,o,G,L1,U1,U2. ⦃G, L1⦄ ⊢ U1 ➡[h, o] U2 →
-                           ∀L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 →
-                           ∀i. L2 ⊢ i ϵ 𝐅*[0]⦃U2⦄ → L1 ⊢ i ϵ 𝐅*[0]⦃U1⦄.
-#h #o #G #L1 #U1 @(fqup_wf_ind_eq … G L1 U1) -G -L1 -U1
-#G0 #L0 #U0 #IH #G #L1 * *
-[ -IH #s #HG #HL #HU #U2 #H1 #L2 #_ #i #H2 elim (cpx_inv_sort1 … H1) -H1
-  [| * #d #_ ] #H destruct elim (frees_inv_sort … H2)
-| #j #HG #HL #HU #U2 #H1 #L2 #HL12 #i #H2 elim (cpx_inv_lref1 … H1) -H1
-  [ #H destruct elim (frees_inv_lref … H2) -H2 //
-    * #I #K2 #W2 #Hj #Hji #HLK2 #HW2
-    elim (lpx_drop_trans_O1 … HL12 … HLK2) -HL12 #Y #HLK1 #H
-    elim (lpx_inv_pair2 … H) -H #K1 #W1 #HK12 #HW12 #H destruct
-    /4 width=11 by frees_lref_be, fqup_lref/
-  | * #I #K1 #W1 #W0 #HLK1 #HW10 #HW0U2
-    lapply (drop_fwd_drop2 … HLK1) #H0
-    elim (lpx_drop_conf … H0 … HL12) -H0 -HL12 #K2 #HK12 #HLK2
-    elim (ylt_split i (j+1)) >yplus_SO2 #Hji
-    [ -IH elim (frees_inv_lift_be … H2 … HLK2 … HW0U2) /2 width=1 by ylt_fwd_succ2/
-    | lapply (frees_inv_lift_ge … H2 … HLK2 … HW0U2 ?) -L2 -U2 // destruct
-      /4 width=11 by frees_lref_be, fqup_lref, yle_succ1_inj/
-    ]
-  ]
-| -IH #p #HG #HL #HU #U2 #H1 >(cpx_inv_gref1 … H1) -H1 destruct
-   #L2 #_ #i #H2 elim (frees_inv_gref … H2)
-| #a #I #W1 #U1 #HG #HL #HU #X #HX #L2 #HL12 #i #Hi destruct
-  elim (cpx_inv_bind1 … HX) -HX *
-  [ #W2 #U2 #HW12 #HU12 #H destruct
-    elim (frees_inv_bind_O … Hi) -Hi
-    /4 width=7 by frees_bind_dx_O, frees_bind_sn, lpx_pair/
-  | #U2 #HU12 #HXU2 #H1 #H2 destruct
-    lapply (frees_lift_ge … Hi (L2.ⓓW1) (Ⓕ) … HXU2 ?)
-    /4 width=7 by frees_bind_dx_O, lpx_pair, drop_drop/
-  ]
-| #I #W1 #X1 #HG #HL #HU #X2 #HX2 #L2 #HL12 #i #Hi destruct
-  elim (cpx_inv_flat1 … HX2) -HX2 *
-  [ #W2 #U2 #HW12 #HU12 #H destruct
-    elim (frees_inv_flat … Hi) -Hi /3 width=7 by frees_flat_dx, frees_flat_sn/
-  | #HU12 #H destruct /3 width=7 by frees_flat_dx/
-  | #HW12 #H destruct /3 width=7 by frees_flat_sn/
-  | #b #W2 #V1 #V2 #U1 #U2 #HW12 #HV12 #HU12 #H1 #H2 #H3 destruct
-    elim (frees_inv_bind … Hi) -Hi #Hi
-    [ elim (frees_inv_flat … Hi) -Hi
-      /4 width=7 by frees_flat_dx, frees_flat_sn, frees_bind_sn/
-    | lapply (lreq_frees_trans … Hi (L2.ⓛV2) ?) /2 width=1 by lreq_succ/ -Hi #HU2
-      lapply (frees_weak … HU2 0 ?) -HU2
-      /5 width=7 by frees_bind_dx_O, frees_flat_dx, lpx_pair/
-    ]
-  | #b #W2 #W0 #V1 #V2 #U1 #U2 #HW12 #HW20 #HV12 #HU12 #H1 #H2 #H3 destruct
-    elim (frees_inv_bind_O … Hi) -Hi #Hi
-    [ /4 width=7 by frees_flat_dx, frees_bind_sn/
-    | elim (frees_inv_flat … Hi) -Hi
-      [ #HW0 lapply (frees_inv_lift_ge … HW0 L2 (Ⓕ) … HW20 ?) -W0
-        /3 width=7 by frees_flat_sn, drop_drop/
-      | /5 width=7 by frees_bind_dx_O, frees_flat_dx, lpx_pair/
-      ]
-    ]
-  ]
-]
-qed-.
-
-lemma cpx_frees_trans: ∀h,o,G. frees_trans (cpx h o G).
-/2 width=8 by lpx_cpx_frees_trans/ 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-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma
index 8edb998d2..fd4ec0ce1 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma
@@ -13,6 +13,8 @@
 (**************************************************************************)
 
 include "ground_2/relocation/rtmap_pushs.ma".
+include "ground_2/relocation/rtmap_coafter.ma".
+include "basic_2/relocation/lifts_lifts.ma".
 include "basic_2/relocation/drops.ma".
 include "basic_2/static/frees.ma".
 
@@ -20,10 +22,24 @@ include "basic_2/static/frees.ma".
 
 (* Advanced properties ******************************************************)
 
-lemma drops_atom_F: ∀f. ⬇*[Ⓕ, f] ⋆ ≡ ⋆.
-#f @drops_atom #H destruct
+lemma frees_lref_atom: ∀L,i. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ → L ⊢ 𝐅*⦃#i⦄ ≡ 𝐈𝐝.
+#L elim L -L /2 width=1 by frees_atom/
+#L #I #V #IH *
+[ #H lapply (drops_fwd_isid … H ?) -H // #H destruct
+| /4 width=3 by frees_lref, drops_inv_drop1/
+]
+qed.
+
+lemma frees_lref_pair: ∀f,K,V. K ⊢ 𝐅*⦃V⦄ ≡ f → 
+                       ∀i,I,L. ⬇*[i] L ≡ K.ⓑ{I}V → L ⊢ 𝐅*⦃#i⦄ ≡ ↑*[i] ⫯f.
+#f #K #V #Hf #i elim i -i
+[ #I #L #H lapply (drops_fwd_isid … H ?) -H /2 width=1 by frees_zero/
+| #i #IH #I #L #H elim (drops_inv_succ … H) -H /3 width=2 by frees_lref/
+]
 qed.
 
+(* Advanced inversion lemmas ************************************************)
+
 lemma frees_inv_lref_drops: ∀i,f,L. L ⊢ 𝐅*⦃#i⦄ ≡ f →
                             (⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ ∧ 𝐈⦃f⦄) ∨
                             ∃∃g,I,K,V. K ⊢ 𝐅*⦃V⦄ ≡ g &
@@ -40,153 +56,64 @@ lemma frees_inv_lref_drops: ∀i,f,L. L ⊢ 𝐅*⦃#i⦄ ≡ f →
 ]
 qed-.
 
+(* Properties with generic slicing for local environments *******************)
 
+(* Inversion lemmas with generic slicing for local environments *************)
 
-lemma frees_dec: ∀L,U,l,i. Decidable (frees l L U i).
-#L #U @(f2_ind … rfw … L U) -L -U
-#x #IH #L * *
-[ -IH /3 width=5 by frees_inv_sort, or_intror/
-| #j #Hx #l #i elim (ylt_split_eq i j) #Hji
-  [ -x @or_intror #H elim (ylt_yle_false … Hji)
-    lapply (frees_inv_lref_ge … H ?) -L -l /2 width=1 by ylt_fwd_le/
-  | -x /2 width=1 by or_introl/
-  | elim (ylt_split j l) #Hli
-    [ -x @or_intror #H elim (ylt_yle_false … Hji)
-      lapply (frees_inv_lref_skip … H ?) -L //
-    | elim (lt_or_ge j (|L|)) #Hj
-      [ elim (drop_O1_lt (Ⓕ) L j) // -Hj #I #K #W #HLK destruct
-        elim (IH K W … 0 (i-j-1)) -IH [1,3: /3 width=5 by frees_lref_be, drop_fwd_rfw, or_introl/ ] #HnW
-        @or_intror #H elim (frees_inv_lref_lt … H) // #Z #Y #X #_ #HLY -l
-        lapply (drop_mono … HLY … HLK) -L #H destruct /2 width=1 by/  
-      | -x @or_intror #H elim (ylt_yle_false … Hji)
-        lapply (frees_inv_lref_free … H ?) -l //
-      ]
-    ]
-  ]
-| -IH /3 width=5 by frees_inv_gref, or_intror/
-| #a #I #W #U #Hx #l #i destruct
-  elim (IH L W … l i) [1,3: /3 width=1 by frees_bind_sn, or_introl/ ] #HnW
-  elim (IH (L.ⓑ{I}W) U … (⫯l) (i+1)) -IH [1,3: /3 width=1 by frees_bind_dx, or_introl/ ] #HnU
-  @or_intror #H elim (frees_inv_bind … H) -H /2 width=1 by/
-| #I #W #U #Hx #l #i destruct
-  elim (IH L W … l i) [1,3: /3 width=1 by frees_flat_sn, or_introl/ ] #HnW
-  elim (IH L U … l i) -IH [1,3: /3 width=1 by frees_flat_dx, or_introl/ ] #HnU
-  @or_intror #H elim (frees_inv_flat … H) -H /2 width=1 by/
-]
-qed-.
-
-lemma frees_S: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[yinj l]⦃U⦄ → ∀I,K,W. ⬇[l] L ≡ K.ⓑ{I}W →
-               (K ⊢ ⫰(i-l) ϵ 𝐅*[0]⦃W⦄ → ⊥) → L ⊢ i ϵ 𝐅*[⫯l]⦃U⦄.
-#L #U #l #i #H elim (frees_inv … H) -H /3 width=2 by frees_eq/
-* #I #K #W #j #Hlj #Hji #HnU #HLK #HW #I0 #K0 #W0 #HLK0 #HnW0
-lapply (yle_inv_inj … Hlj) -Hlj #Hlj
-elim (le_to_or_lt_eq … Hlj) -Hlj
-[ -I0 -K0 -W0 /3 width=9 by frees_be, yle_inj/
-| -Hji -HnU #H destruct
-  lapply (drop_mono … HLK0 … HLK) #H destruct -I
-  elim HnW0 -L -U -HnW0 //
-]
-qed.
-
-(* Note: lemma 1250 *)
-lemma frees_bind_dx_O: ∀a,I,L,W,U,i. L.ⓑ{I}W ⊢ ⫯i ϵ 𝐅*[0]⦃U⦄ →
-                       L ⊢ i ϵ 𝐅*[0]⦃ⓑ{a,I}W.U⦄.
-#a #I #L #W #U #i #HU elim (frees_dec L W 0 i)
-/4 width=5 by frees_S, frees_bind_dx, frees_bind_sn/
-qed.
-
-(* Properties on relocation *************************************************)
-
-lemma frees_lift_ge: ∀K,T,l,i. K ⊢ i ϵ𝐅*[l]⦃T⦄ →
-                     ∀L,s,l0,m0. ⬇[s, l0, m0] L ≡ K →
-                     ∀U. ⬆[l0, m0] T ≡ U → l0 ≤ i →
-                     L ⊢ i+m0 ϵ 𝐅*[l]⦃U⦄.
-#K #T #l #i #H elim H -K -T -l -i
-[ #K #T #l #i #HnT #L #s #l0 #m0 #_ #U #HTU #Hl0i -K -s
-  @frees_eq #X #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
-| #I #K #K0 #T #V #l #i #j #Hlj #Hji #HnT #HK0 #HV #IHV #L #s #l0 #m0 #HLK #U #HTU #Hl0i
-  elim (ylt_split j l0) #H0
-  [ elim (drop_trans_lt … HLK … HK0) // -K #L0 #W #HL0 >yminus_SO2 #HLK0 #HVW
-    @(frees_be … HL0) -HL0 -HV /3 width=3 by ylt_plus_dx2_trans/
-    [ lapply (ylt_fwd_lt_O1 … H0) #H1
-      #X #HXU <(ymax_pre_sn l0 1) in HTU; /2 width=1 by ylt_fwd_le_succ1/ #HTU
-      <(ylt_inv_O1 l0) in H0; // -H1 #H0
-      elim (lift_div_le … HXU … HTU ?) -U /2 width=2 by ylt_fwd_succ2/
-    | >yplus_minus_comm_inj /2 width=1 by ylt_fwd_le/
-      <yplus_pred1 /4 width=5 by monotonic_yle_minus_dx, yle_pred, ylt_to_minus/
-    ]
-  | lapply (drop_trans_ge … HLK … HK0 ?) // -K #HLK0
-    lapply (drop_inv_gen … HLK0) >commutative_plus -HLK0 #HLK0
-    @(frees_be … HLK0) -HLK0 -IHV
-    /2 width=1 by monotonic_ylt_plus_dx, yle_plus_dx1_trans/
-    [ #X <yplus_inj #HXU elim (lift_div_le … HTU … HXU) -U /2 width=2 by/
-    | <yplus_minus_assoc_comm_inj //
-    ]
-  ]
-]
-qed.
-
-(* Inversion lemmas on relocation *******************************************)
-
-lemma frees_inv_lift_be: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
-                         ∀K,s,l0,m0. ⬇[s, l0, m0+1] L ≡ K →
-                         ∀T. ⬆[l0, m0+1] T ≡ U → l0 ≤ i → i ≤ l0 + m0 → ⊥.
-#L #U #l #i #H elim H -L -U -l -i
-[ #L #U #l #i #HnU #K #s #l0 #m0 #_ #T #HTU #Hl0i #Hilm0
-  elim (lift_split … HTU i m0) -HTU /2 width=2 by/
-| #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hl0i #Hilm0
-  elim (ylt_split j l0) #H1
-  [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
-    @(IHW … HKL0 … HVW)
-    [ /3 width=1 by monotonic_yle_minus_dx, yle_pred/
-    | >yplus_pred1 /2 width=1 by ylt_to_minus/
-      <yplus_minus_comm_inj /3 width=1 by monotonic_yle_minus_dx, yle_pred, ylt_fwd_le/
-    ]
-  | elim (lift_split … HTU j m0) -HTU /3 width=3 by ylt_yle_trans, ylt_fwd_le/
-  ]
-]
-qed-.
-
-lemma frees_inv_lift_ge: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ →
-                         ∀K,s,l0,m0. ⬇[s, l0, m0] L ≡ K →
-                         ∀T. ⬆[l0, m0] T ≡ U → l0 + m0 ≤ i →
-                         K ⊢ i-m0 ϵ𝐅*[l-yinj m0]⦃T⦄.
-#L #U #l #i #H elim H -L -U -l -i
-[ #L #U #l #i #HnU #K #s #l0 #m0 #HLK #T #HTU #Hlm0i -L -s
-  elim (yle_inv_plus_inj2 … Hlm0i) -Hlm0i #Hl0im0 #Hm0i @frees_eq #X #HXT -K
-  elim (lift_trans_le … HXT … HTU) -T // >ymax_pre_sn /2 width=2 by/
-| #I #L #K0 #U #W #l #i #j #Hli #Hij #HnU #HLK0 #_ #IHW #K #s #l0 #m0 #HLK #T #HTU #Hlm0i
-  elim (ylt_split j l0) #H1
-  [ elim (drop_conf_lt … HLK … HLK0) -L // #L0 #V #H #HKL0 #HVW
-    elim (yle_inv_plus_inj2 … Hlm0i) #H0 #Hm0i
-    @(frees_be … H) -H
-    [ /3 width=1 by yle_plus_dx1_trans, monotonic_yle_minus_dx/
-    | /2 width=3 by ylt_yle_trans/
-    | #X #HXT elim (lift_trans_ge … HXT … HTU) -T /2 width=2 by ylt_fwd_le_succ1/
-    | lapply (IHW … HKL0 … HVW ?) // -I -K -K0 -L0 -V -W -T -U -s
-      >yplus_pred1 /2 width=1 by ylt_to_minus/
-      <yplus_minus_comm_inj /3 width=1 by monotonic_yle_minus_dx, yle_pred, ylt_fwd_le/
-    ]
-  | elim (ylt_split j (l0+m0)) #H2
-    [ -L -I -W elim (yle_inv_inj2 … H1) -H1 #x #H1 #H destruct
-      lapply (ylt_plus2_to_minus_inj1 … H2) /2 width=1 by yle_inj/ #H3
-      lapply (ylt_fwd_lt_O1 … H3) -H3 #H3
-      elim (lift_split … HTU j (m0-1)) -HTU /2 width=1 by yle_inj/
-      [ >minus_minus_associative /2 width=1 by ylt_inv_inj/ <minus_n_n
-        -H2 #X #_ #H elim (HnU … H)
-      | <yminus_inj >yminus_SO2 >yplus_pred2 /2 width=1 by ylt_fwd_le_pred2/
-      ]
-    | lapply (drop_conf_ge … HLK … HLK0 ?) // -L #HK0
-      elim ( yle_inv_plus_inj2 … H2) -H2 #H2 #Hm0j
-      @(frees_be … HK0)
-      [ /2 width=1 by monotonic_yle_minus_dx/
-      | /2 width=1 by monotonic_ylt_minus_dx/
-      | #X #HXT elim (lift_trans_le … HXT … HTU) -T //
-        <yminus_inj >ymax_pre_sn /2 width=2 by/
-      | <yminus_inj >yplus_minus_assoc_comm_inj //
-        >ymax_pre_sn /3 width=5 by yle_trans, ylt_fwd_le/
-      ]
-    ]
-  ]
+lemma frees_inv_lifts: ∀b,f2,L,U. L ⊢ 𝐅*⦃U⦄ ≡ f2 →
+                       ∀f,K. ⬇*[b, f] L ≡ K → ∀T. ⬆*[f] T ≡ U →
+                       ∀f1. f ~⊚ f1 ≡ f2 → K ⊢ 𝐅*⦃T⦄ ≡ f1.
+#b #f2 #L #U #H lapply (frees_fwd_isfin … H) elim H -f2 -L -U
+[ #f2 #I #Hf2 #_ #f #K #H1 #T #H2 #f1 #H3
+  lapply (coafter_fwd_isid2 … H3 … Hf2) -H3 // -Hf2 #Hf1
+  elim (drops_inv_atom1 … H1) -H1 #H #_ destruct
+  elim (lifts_fwd_atom2 … H2) -H2
+  /2 width=3 by frees_atom/
+| #f2 #I #L #W #s #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3
+  lapply (isfin_fwd_push … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+  lapply (lifts_inv_sort2 … H2) -H2 #H destruct
+  elim (coafter_inv_xxp … H3) -H3 [1,3: * |*: // ]
+  [ #g #g1 #Hf2 #H #H0 destruct
+    elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #_ #H destruct
+  | #g #Hf2 #H destruct
+    lapply (drops_inv_drop1 … H1) -H1
+  ] /3 width=4 by frees_sort/
+| #f2 #I #L #W #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3
+  lapply (isfin_inv_next … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+  elim (lifts_inv_lref2 … H2) -H2 #i #H2 #H destruct
+  lapply (at_inv_xxp … H2 ?) -H2 // * #g #H #H0 destruct
+  elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #HVW #H destruct
+  elim (coafter_inv_pxn … H3) -H3 [ |*: // ] #g1 #Hf2 #H destruct
+  /3 width=4 by frees_zero/
+| #f2 #I #L #W #j #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3
+  lapply (isfin_fwd_push … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+  elim (lifts_inv_lref2 … H2) -H2 #x #H2 #H destruct
+  elim (coafter_inv_xxp … H3) -H3 [1,3: * |*: // ]
+  [ #g #g1 #Hf2 #H #H0 destruct
+    elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #HVW #H destruct
+    elim (at_inv_xpn … H2) -H2 [ |*: // ] #j #Hg #H destruct
+  | #g #Hf2 #H destruct
+    lapply (drops_inv_drop1 … H1) -H1
+    lapply (at_inv_xnn … H2 ????) -H2 [5: |*: // ]
+  ] /4 width=4 by lifts_lref, frees_lref/
+| #f2 #I #L #W #l #_ #IH #Hf2 #f #Y #H1 #T #H2 #f1 #H3
+  lapply (isfin_fwd_push … Hf2 ??) -Hf2 [3: |*: // ] #Hf2
+  lapply (lifts_inv_gref2 … H2) -H2 #H destruct
+  elim (coafter_inv_xxp … H3) -H3 [1,3: * |*: // ]
+  [ #g #g1 #Hf2 #H #H0 destruct
+    elim (drops_inv_skip1 … H1) -H1 #K #V #HLK #_ #H destruct
+  | #g #Hf2 #H destruct
+    lapply (drops_inv_drop1 … H1) -H1
+  ] /3 width=4 by frees_gref/
+| #f2W #f2U #f2 #p #I #L #W #U #_ #_ #H1f2 #IHW #IHU #H2f2 #f #K #H1 #X #H2 #f1 #H3
+  elim (sor_inv_isfin3 … H1f2) // #H1f2W #H
+  lapply (isfin_inv_tl … H) -H
+  elim (lifts_inv_bind2 … H2) -H2 #V #T #HVW #HTU #H destruct
+  elim (coafter_inv_sor … H3 … H1f2) -H3 -H1f2 // #f1W #f1U #H2f2W #H
+  elim (coafter_inv_tl0 … H) -H /4 width=5 by frees_bind, drops_skip/
+| #f2W #f2U #f2 #I #L #W #U #_ #_ #H1f2 #IHW #IHU #H2f2 #f #K #H1 #X #H2 #f1 #H3
+  elim (sor_inv_isfin3 … H1f2) //
+  elim (lifts_inv_flat2 … H2) -H2 #V #T #HVW #HTU #H destruct
+  elim (coafter_inv_sor … H3 … H1f2) -H3 -H1f2 /3 width=5 by frees_flat/
 ]
 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 852d6bce3..56c217b56 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
@@ -190,7 +190,7 @@ table {
           }
         ]
         [ { "context-sensitive free variables" * } {
-             [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_lreq" + "frees_frees" * ]
+             [ "frees ( ? ⊢ 𝐅*⦃?⦄ ≡ ? )" "frees_weight" + "frees_lreq" + "frees_drops" + "frees_frees" * ]
           }
         ]
      }
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
index ad5242bb6..c58db6ec0 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_coafter.ma
@@ -275,6 +275,16 @@ lemma coafter_mono_eq: ∀f1,f2,f. f1 ~⊚ f2 ≡ f → ∀g1,g2,g. g1 ~⊚ g2 
                        f1 ≗ g1 → f2 ≗ g2 → f ≗ g.
 /4 width=4 by coafter_mono, coafter_eq_repl_back1, coafter_eq_repl_back2/ qed-.
 
+(* Inversion lemmas with tail ***********************************************)
+
+lemma coafter_inv_tl0: ∀g2,g1,g. g2 ~⊚ g1 ≡ ⫱g →
+                       ∃∃f1. ↑g2 ~⊚ f1 ≡ g & ⫱f1 = g1.
+#g1 #g2 #g elim (pn_split g) * #f #H0 #H destruct
+[ /3 width=7 by coafter_refl, ex2_intro/
+| @(ex2_intro … (⫯g2)) /2 width=7 by coafter_push/ (**) (* full auto fails *)
+]
+qed-.
+
 (* Properties on tls ********************************************************)
 
 lemma coafter_tls: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n →
diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma
index 0c9a65bf2..8a127b359 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_isfin.ma
@@ -70,3 +70,9 @@ lemma isfin_tl: ∀f. 𝐅⦃f⦄ → 𝐅⦃⫱f⦄.
 #f elim (pn_split f) * #g #H #Hf destruct
 /3 width=3 by isfin_fwd_push, isfin_inv_next/
 qed.
+
+(* Inversion lemmas with tail ***********************************************)
+
+lemma isfin_inv_tl: ∀f. 𝐅⦃⫱f⦄ → 𝐅⦃f⦄.
+#f elim (pn_split f) * /2 width=1 by isfin_next, isfin_push/   
+qed-.
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 32fea4954..3ae50a862 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_sor.ma
@@ -330,6 +330,25 @@ lemma sor_fcla: ∀f1,n1. 𝐂⦃f1⦄ ≡ n1 → ∀f2,n2. 𝐂⦃f2⦄ ≡ n2
 /4 width=6 by sor_mono, fcla_eq_repl_back, ex3_intro/
 qed-.
 
+(* Forward lemmas with finite colength **************************************)
+
+lemma sor_fwd_fcla_sn_ex: ∀f,n. 𝐂⦃f⦄ ≡ n → ∀f1,f2. f1 ⋓ f2 ≡ f →
+                          ∃∃n1.  𝐂⦃f1⦄ ≡ n1 & n1 ≤ n.
+#f #n #H elim H -f -n
+[ /4 width=4 by sor_fwd_isid1, fcla_isid, ex2_intro/
+| #f #n #_ #IH #f1 #f2 #H
+  elim (sor_inv_xxp … H) -H [ |*: // ] #g1 #g2 #Hf #H1 #H2 destruct
+  elim (IH … Hf) -f /3 width=3 by fcla_push, ex2_intro/
+| #f #n #_ #IH #f1 #f2 #H
+  elim (sor_inv_xxn … H) -H [1,3,4: * |*: // ] #g1 #g2 #Hf #H1 #H2 destruct
+  elim (IH … Hf) -f /3 width=3 by fcla_push, fcla_next, le_S_S, le_S, ex2_intro/
+]
+qed-.
+
+lemma sor_fwd_fcla_dx_ex: ∀f,n. 𝐂⦃f⦄ ≡ n → ∀f1,f2. f1 ⋓ f2 ≡ f →
+                          ∃∃n2.  𝐂⦃f2⦄ ≡ n2 & n2 ≤ n.
+/3 width=4 by sor_fwd_fcla_sn_ex, sor_sym/ qed-.
+
 (* Properties on test for finite colength ***********************************)
 
 lemma sor_isfin_ex: ∀f1,f2. 𝐅⦃f1⦄ → 𝐅⦃f2⦄ → ∃∃f. f1 ⋓ f2 ≡ f & 𝐅⦃f⦄.
@@ -342,6 +361,23 @@ lemma sor_isfin: ∀f1,f2. 𝐅⦃f1⦄ → 𝐅⦃f2⦄ → ∀f. f1 ⋓ f2 ≡
 /3 width=6 by sor_mono, isfin_eq_repl_back/
 qed-.
 
+(* Forward lemmas with test for finite colength *****************************)
+
+lemma sor_fwd_isfin_sn: ∀f. 𝐅⦃f⦄ → ∀f1,f2. f1 ⋓ f2 ≡ f → 𝐅⦃f1⦄.
+#f * #n #Hf #f1 #f2 #H
+elim (sor_fwd_fcla_sn_ex … Hf … H) -f -f2 /2 width=2 by ex_intro/
+qed-.
+
+lemma sor_fwd_isfin_dx: ∀f. 𝐅⦃f⦄ → ∀f1,f2. f1 ⋓ f2 ≡ f → 𝐅⦃f2⦄.
+#f * #n #Hf #f1 #f2 #H
+elim (sor_fwd_fcla_dx_ex … Hf … H) -f -f1 /2 width=2 by ex_intro/
+qed-.
+
+(* Inversion lemmas with test for finite colength ***************************)
+
+lemma sor_inv_isfin3: ∀f1,f2,f. f1 ⋓ f2 ≡ f → 𝐅⦃f⦄ → 𝐅⦃f1⦄ ∧ 𝐅⦃f2⦄.
+/3 width=4 by sor_fwd_isfin_dx, sor_fwd_isfin_sn, conj/ qed-.
+
 (* Inversion lemmas on inclusion ********************************************)
 
 corec lemma sor_inv_sle_sn: ∀f1,f2,f. f1 ⋓ f2 ≡ f → f1 ⊆ f.