From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 28 Dec 2022 16:47:38 +0000 (+0100)
Subject: update in delayed_updating
X-Git-Tag: make_still_working~15
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2815c74c03f38089d0e27aba00e2280223b0f76f;p=helm.git

update in delayed_updating

+ some renaming
---

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
index 387dc8f15..48b6d1dfd 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_ibfr.ma
@@ -15,11 +15,11 @@
 include "delayed_updating/reduction/dbfr.ma".
 include "delayed_updating/reduction/ibfr.ma".
 
-include "delayed_updating/unwind/unwind2_prototerm_constructors.ma".
-include "delayed_updating/unwind/unwind2_preterm_fsubst.ma".
-include "delayed_updating/unwind/unwind2_preterm_eq.ma".
-include "delayed_updating/unwind/unwind2_prototerm_lift.ma".
-include "delayed_updating/unwind/unwind2_rmap_crux.ma".
+include "delayed_updating/unwind_k/unwind2_prototerm_constructors.ma".
+include "delayed_updating/unwind_k/unwind2_preterm_fsubst.ma".
+include "delayed_updating/unwind_k/unwind2_preterm_eq.ma".
+include "delayed_updating/unwind_k/unwind2_prototerm_lift.ma".
+include "delayed_updating/unwind_k/unwind2_rmap_crux.ma".
 
 include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_eq.ma".
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected_neg.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected_neg.ma
index a83a71d5f..ed87aa714 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected_neg.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dbfr_unprotected_neg.ma
@@ -14,7 +14,7 @@
 
 include "delayed_updating/reduction/dbfr_constructors.ma".
 include "delayed_updating/reduction/ibfr_constructors.ma".
-include "delayed_updating/unwind/unwind2_prototerm_constructors.ma".
+include "delayed_updating/unwind_k/unwind2_prototerm_constructors.ma".
 include "delayed_updating/substitution/lift_prototerm_constructors.ma".
 include "ground/arith/pnat_two.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma
index 34feec243..56cfaa6ca 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ibfr_unwind.ma
@@ -14,10 +14,10 @@
 
 include "delayed_updating/reduction/ibfr.ma".
 
-include "delayed_updating/unwind/unwind2_preterm_fsubst.ma".
-include "delayed_updating/unwind/unwind2_preterm_eq.ma".
-include "delayed_updating/unwind/unwind2_prototerm_lift.ma".
-include "delayed_updating/unwind/unwind2_rmap_crux.ma".
+include "delayed_updating/unwind_k/unwind2_preterm_fsubst.ma".
+include "delayed_updating/unwind_k/unwind2_preterm_eq.ma".
+include "delayed_updating/unwind_k/unwind2_prototerm_lift.ma".
+include "delayed_updating/unwind_k/unwind2_rmap_crux.ma".
 
 include "delayed_updating/substitution/fsubst_eq.ma".
 include "delayed_updating/substitution/lift_prototerm_eq.ma".
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap.ma
deleted file mode 100644
index d6cdbce3d..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap.ma
+++ /dev/null
@@ -1,55 +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 "delayed_updating/syntax/label.ma".
-include "delayed_updating/notation/functions/black_righttriangle_2.ma".
-include "ground/relocation/tr_uni.ma".
-include "ground/relocation/tr_compose.ma".
-
-(* TAILED PREUNWIND FOR RELOCATION MAP **************************************)
-
-definition preunwind2_rmap (f) (l): tr_map ≝
-match l with
-[ label_d k ⇒ f∘𝐮❨k❩
-| label_m   ⇒ f
-| label_L   ⇒ ⫯f
-| label_A   ⇒ f
-| label_S   ⇒ f
-].
-
-interpretation
-  "tailed preunwind (relocation map)"
-  'BlackRightTriangle f l = (preunwind2_rmap f l).
-
-(* Basic constructions ******************************************************)
-
-lemma preunwind2_rmap_d (f) (k:pnat):
-      f∘𝐮❨k❩ = ▶[f]𝗱k.
-// qed.
-
-lemma preunwind2_rmap_m (f):
-      f = ▶[f]𝗺.
-// qed.
-
-lemma preunwind2_rmap_L (f):
-      (⫯f) = ▶[f]𝗟.
-// qed.
-
-lemma preunwind2_rmap_A (f):
-      f = ▶[f]𝗔.
-// qed.
-
-lemma preunwind2_rmap_S (f):
-      f = ▶[f]𝗦.
-// qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_eq.ma
deleted file mode 100644
index 32efd9f04..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_eq.ma
+++ /dev/null
@@ -1,27 +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 "delayed_updating/unwind/preunwind2_rmap.ma".
-include "ground/relocation/tr_compose_eq.ma".
-include "ground/relocation/tr_pn_eq.ma".
-
-(* TAILED PREUNWIND FOR RELOCATION MAP **************************************)
-
-(* Constructions with tr_map_eq *********************************************)
-
-lemma preunwind2_rmap_eq_repl (l):
-      stream_eq_repl … (λf1,f2. ▶[f1]l ≗ ▶[f2]l).
-* // #k #f1 #f2 #Hf
-/2 width=1 by tr_compose_eq_repl/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_lift.ma
deleted file mode 100644
index cc5b351ad..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_lift.ma
+++ /dev/null
@@ -1,34 +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 "delayed_updating/unwind/preunwind2_rmap.ma".
-include "delayed_updating/substitution/prelift_label.ma".
-include "delayed_updating/substitution/prelift_rmap.ma".
-include "ground/relocation/tr_uni_compose.ma".
-include "ground/relocation/tr_compose_compose.ma".
-include "ground/relocation/tr_compose_eq.ma".
-include "ground/lib/stream_eq_eq.ma".
-
-(* TAILED PREUNWIND FOR RELOCATION MAP **************************************)
-
-(* Constructions with lift_path *********************************************)
-
-lemma preunwind2_lift_rmap_after (g) (f) (l):
-      ▶[g]🠡[f]l∘🠢[f]l ≗ ▶[g∘f]l.
-#g #f * // #k
-<prelift_label_d <prelift_rmap_d <preunwind2_rmap_d <preunwind2_rmap_d
-@(stream_eq_trans … (tr_compose_assoc …))
-@(stream_eq_canc_dx … (tr_compose_assoc …))
-/2 width=1 by tr_compose_eq_repl/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path.ma
deleted file mode 100644
index 08115e1e4..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path.ma
+++ /dev/null
@@ -1,170 +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 "delayed_updating/unwind/unwind2_rmap.ma".
-include "delayed_updating/syntax/path_structure.ma".
-include "delayed_updating/notation/functions/black_downtriangle_2.ma".
-
-(* TAILED UNWIND FOR PATH ***************************************************)
-
-definition unwind2_path (f) (p): path ≝
-match p with
-[ list_empty     ⇒ (𝐞)
-| list_lcons l q ⇒
-  match l with
-  [ label_d k ⇒ (⊗q)◖𝗱(▶[f]q＠⧣❨k❩)
-  | label_m   ⇒ ⊗p
-  | label_L   ⇒ ⊗p
-  | label_A   ⇒ ⊗p
-  | label_S   ⇒ ⊗p
-  ]
-].
-
-interpretation
-  "tailed unwind (path)"
-  'BlackDownTriangle f p = (unwind2_path f p).
-
-(* Basic constructions ******************************************************)
-
-lemma unwind2_path_empty (f):
-      (𝐞) = ▼[f]𝐞.
-// qed.
-
-lemma unwind2_path_d_dx (f) (p) (k) :
-      (⊗p)◖𝗱((▶[f]p)＠⧣❨k❩) = ▼[f](p◖𝗱k).
-// qed.
-
-lemma unwind2_path_m_dx (f) (p):
-      ⊗p = ▼[f](p◖𝗺).
-// qed.
-
-lemma unwind2_path_L_dx (f) (p):
-      (⊗p)◖𝗟 = ▼[f](p◖𝗟).
-// qed.
-
-lemma unwind2_path_A_dx (f) (p):
-      (⊗p)◖𝗔 = ▼[f](p◖𝗔).
-// qed.
-
-lemma unwind2_path_S_dx (f) (p):
-      (⊗p)◖𝗦 = ▼[f](p◖𝗦).
-// qed.
-
-(* Constructions with structure *********************************************)
-
-lemma structure_unwind2_path (f) (p):
-      ⊗p = ⊗▼[f]p.
-#f * // * [ #k ] #p //
-qed.
-
-lemma unwind2_path_structure (f) (p):
-      ⊗p = ▼[f]⊗p.
-#f #p elim p -p // * [ #k ] #p #IH //
-[ <structure_L_dx <unwind2_path_L_dx //
-| <structure_A_dx <unwind2_path_A_dx //
-| <structure_S_dx <unwind2_path_S_dx //
-]
-qed.
-
-lemma unwind2_path_root (f) (p):
-      ∃∃r. 𝐞 = ⊗r & ⊗p●r = ▼[f]p.
-#f * [| * [ #k ] #p ]
-/2 width=3 by ex2_intro/
-<unwind2_path_d_dx <structure_d_dx
-/2 width=3 by ex2_intro/
-qed-.
-
-(* Destructions with structure **********************************************)
-
-lemma unwind2_path_des_structure (f) (q) (p):
-      ⊗q = ▼[f]p → ⊗q = ⊗p.
-// qed-.
-
-(* Basic inversions *********************************************************)
-
-lemma eq_inv_d_dx_unwind2_path (f) (q) (p) (h):
-      q◖𝗱h = ▼[f]p →
-      ∃∃r,k. q = ⊗r & h = ▶[f]r＠⧣❨k❩ & r◖𝗱k = p.
-#f #q * [| * [ #k ] #p ] #h
-[ <unwind2_path_empty #H0 destruct
-| <unwind2_path_d_dx #H0 destruct
-  /2 width=5 by ex3_2_intro/
-| <unwind2_path_m_dx #H0
-  elim (eq_inv_d_dx_structure … H0)
-| <unwind2_path_L_dx #H0 destruct
-| <unwind2_path_A_dx #H0 destruct
-| <unwind2_path_S_dx #H0 destruct
-]
-qed-.
-
-lemma eq_inv_m_dx_unwind2_path (f) (q) (p):
-      q◖𝗺 = ▼[f]p → ⊥.
-#f #q * [| * [ #k ] #p ]
-[ <unwind2_path_empty #H0 destruct
-| <unwind2_path_d_dx #H0 destruct
-| <unwind2_path_m_dx #H0
-  elim (eq_inv_m_dx_structure … H0)
-| <unwind2_path_L_dx #H0 destruct
-| <unwind2_path_A_dx #H0 destruct
-| <unwind2_path_S_dx #H0 destruct
-]
-qed-.
-
-lemma eq_inv_L_dx_unwind2_path (f) (q) (p):
-      q◖𝗟 = ▼[f]p →
-      ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗟◗r2 = p.
-#f #q * [| * [ #k ] #p ]
-[ <unwind2_path_empty #H0 destruct
-| <unwind2_path_d_dx #H0 destruct
-| <unwind2_path_m_dx #H0
-  elim (eq_inv_L_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
-  /2 width=5 by ex3_2_intro/
-| <unwind2_path_L_dx #H0 destruct
-  /2 width=5 by ex3_2_intro/
-| <unwind2_path_A_dx #H0 destruct
-| <unwind2_path_S_dx #H0 destruct
-]
-qed-.
-
-lemma eq_inv_A_dx_unwind2_path (f) (q) (p):
-      q◖𝗔 = ▼[f]p →
-      ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗔◗r2 = p.
-#f #q * [| * [ #k ] #p ]
-[ <unwind2_path_empty #H0 destruct
-| <unwind2_path_d_dx #H0 destruct
-| <unwind2_path_m_dx #H0
-  elim (eq_inv_A_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
-  /2 width=5 by ex3_2_intro/
-| <unwind2_path_L_dx #H0 destruct
-| <unwind2_path_A_dx #H0 destruct
-  /2 width=5 by ex3_2_intro/
-| <unwind2_path_S_dx #H0 destruct
-]
-qed-.
-
-lemma eq_inv_S_dx_unwind2_path (f) (q) (p):
-      q◖𝗦 = ▼[f]p →
-      ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗦◗r2 = p.
-#f #q * [| * [ #k ] #p ]
-[ <unwind2_path_empty #H0 destruct
-| <unwind2_path_d_dx #H0 destruct
-| <unwind2_path_m_dx #H0
-  elim (eq_inv_S_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
-  /2 width=5 by ex3_2_intro/
-| <unwind2_path_L_dx #H0 destruct
-| <unwind2_path_A_dx #H0 destruct
-| <unwind2_path_S_dx #H0 destruct
-  /2 width=5 by ex3_2_intro/
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_after.ma
deleted file mode 100644
index c7a3bcf0f..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_after.ma
+++ /dev/null
@@ -1,28 +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 "delayed_updating/unwind/unwind2_path_eq.ma".
-include "delayed_updating/unwind/unwind2_rmap_after.ma".
-
-(* TAILED UNWIND FOR PATH ***************************************************)
-
-(* Properties with tr_after *************************************************)
-
-lemma unwind2_path_after (g) (f) (p):
-      ▼[g]▼[f]p = ▼[g∘f]p.
-#g #f * // * [ #k ] #p //
-<unwind2_path_d_dx <unwind2_path_d_dx
-@eq_f2 // @eq_f >tr_compose_pap
-/2 width=3 by tr_pap_eq_repl/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma
deleted file mode 100644
index 8796ce86f..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma
+++ /dev/null
@@ -1,244 +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 "delayed_updating/unwind/unwind2_path.ma".
-include "delayed_updating/syntax/path_inner.ma".
-include "delayed_updating/syntax/path_proper.ma".
-include "ground/xoa/ex_4_2.ma".
-
-(* TAILED UNWIND FOR PATH ***************************************************)
-
-(* Constructions with pic ***************************************************)
-
-lemma unwind2_path_pic (f) (p):
-      p ϵ 𝐈 → ⊗p = ▼[f]p.
-#f * // * // #k #q #Hq
-elim (pic_inv_d_dx … Hq)
-qed-.
-
-(* Constructions with append and pic ****************************************)
-
-lemma unwind2_path_append_pic_sn (f) (p) (q): p ϵ 𝐈 →
-      (⊗p)●(▼[▶[f]p]q) = ▼[f](p●q).
-#f #p * [ #Hp | * [ #k ] #q #_ ] //
-[ <(unwind2_path_pic … Hp) -Hp //
-| <unwind2_path_d_dx <unwind2_path_d_dx
-  /2 width=3 by trans_eq/
-| <unwind2_path_L_dx <unwind2_path_L_dx //
-| <unwind2_path_A_dx <unwind2_path_A_dx //
-| <unwind2_path_S_dx <unwind2_path_S_dx //
-]
-qed.
-
-(* Constructions with append and ppc ****************************************)
-
-lemma unwind2_path_append_ppc_dx (f) (p) (q): q ϵ 𝐏 →
-      (⊗p)●(▼[▶[f]p]q) = ▼[f](p●q).
-#f #p * [ #Hq | * [ #k ] #q #_ ] //
-[ elim (ppc_inv_empty … Hq)
-| <unwind2_path_d_dx <unwind2_path_d_dx
-  /2 width=3 by trans_eq/
-| <unwind2_path_L_dx <unwind2_path_L_dx //
-| <unwind2_path_A_dx <unwind2_path_A_dx //
-| <unwind2_path_S_dx <unwind2_path_S_dx //
-]
-qed.
-
-(* Constructions with path_lcons ********************************************)
-
-lemma unwind2_path_d_empty (f) (k):
-      (𝗱(f＠⧣❨k❩)◗𝐞) = ▼[f](𝗱k◗𝐞).
-// qed.
-
-lemma unwind2_path_d_lcons (f) (p) (l) (k:pnat):
-      ▼[f∘𝐮❨k❩](l◗p) = ▼[f](𝗱k◗l◗p).
-#f #p #l #k <unwind2_path_append_ppc_dx in ⊢ (???%); //
-qed.
-
-lemma unwind2_path_m_sn (f) (p):
-      ▼[f]p = ▼[f](𝗺◗p).
-#f #p <unwind2_path_append_pic_sn //
-qed.
-
-lemma unwind2_path_L_sn (f) (p):
-      (𝗟◗▼[⫯f]p) = ▼[f](𝗟◗p).
-#f #p <unwind2_path_append_pic_sn //
-qed.
-
-lemma unwind2_path_A_sn (f) (p):
-      (𝗔◗▼[f]p) = ▼[f](𝗔◗p).
-#f #p <unwind2_path_append_pic_sn //
-qed.
-
-lemma unwind2_path_S_sn (f) (p):
-      (𝗦◗▼[f]p) = ▼[f](𝗦◗p).
-#f #p <unwind2_path_append_pic_sn //
-qed.
-
-(* Destructions with pic ****************************************************)
-
-lemma unwind2_path_des_pic (f) (p):
-      ▼[f]p ϵ 𝐈 → p ϵ 𝐈.
-#f * // * [ #k ] #p //
-<unwind2_path_d_dx #H0
-elim (pic_inv_d_dx … H0)
-qed-.
-
-(* Destructions with append and pic *****************************************)
-
-lemma unwind2_path_des_append_pic_sn (f) (p) (q1) (q2):
-      q1 ϵ 𝐈 → q1●q2 = ▼[f]p →
-      ∃∃p1,p2. q1 = ⊗p1 & q2 = ▼[▶[f]p1]p2 & p1●p2 = p.
-#f #p #q1 * [| * [ #k ] #q2 ] #Hq1
-[ <list_append_empty_sn #H0 destruct
-  lapply (unwind2_path_des_pic … Hq1) -Hq1 #Hp
-  <(unwind2_path_pic … Hp) -Hp
-  /2 width=5 by ex3_2_intro/
-| #H0 elim (eq_inv_d_dx_unwind2_path … H0) -H0 #r #h #Hr #H1 #H2 destruct
-  elim (eq_inv_append_structure … Hr) -Hr #s1 #s2 #H1 #H2 #H3 destruct
-  /2 width=5 by ex3_2_intro/
-| #H0 elim (eq_inv_m_dx_unwind2_path … H0)
-| #H0 elim (eq_inv_L_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
-  elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
-  @(ex3_2_intro … s1 (s2●𝗟◗r2)) //
-  <unwind2_path_append_ppc_dx //
-  <unwind2_path_L_sn <Hr2 -Hr2 //
-| #H0 elim (eq_inv_A_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
-  elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
-  @(ex3_2_intro … s1 (s2●𝗔◗r2)) //
-  <unwind2_path_append_ppc_dx //
-  <unwind2_path_A_sn <Hr2 -Hr2 //
-| #H0 elim (eq_inv_S_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
-  elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
-  @(ex3_2_intro … s1 (s2●𝗦◗r2)) //
-  <unwind2_path_append_ppc_dx //
-  <unwind2_path_S_sn <Hr2 -Hr2 //
-]
-qed-.
-
-(* Inversions with append and ppc *******************************************)
-
-lemma unwind2_path_inv_append_ppc_dx (f) (p) (q1) (q2):
-      q2 ϵ 𝐏 → q1●q2 = ▼[f]p →
-      ∃∃p1,p2. q1 = ⊗p1 & q2 = ▼[▶[f]p1]p2 & p1●p2 = p.
-#f #p #q1 * [| * [ #k ] #q2 ] #Hq1
-[ <list_append_empty_sn #H0 destruct
-  elim (ppc_inv_empty … Hq1)
-| #H0 elim (eq_inv_d_dx_unwind2_path … H0) -H0 #r #h #Hr #H1 #H2 destruct
-  elim (eq_inv_append_structure … Hr) -Hr #s1 #s2 #H1 #H2 #H3 destruct
-  /2 width=5 by ex3_2_intro/
-| #H0 elim (eq_inv_m_dx_unwind2_path … H0)
-| #H0 elim (eq_inv_L_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
-  elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
-  @(ex3_2_intro … s1 (s2●𝗟◗r2)) //
-  <unwind2_path_append_ppc_dx //
-  <unwind2_path_L_sn <Hr2 -Hr2 //
-| #H0 elim (eq_inv_A_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
-  elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
-  @(ex3_2_intro … s1 (s2●𝗔◗r2)) //
-  <unwind2_path_append_ppc_dx //
-  <unwind2_path_A_sn <Hr2 -Hr2 //
-| #H0 elim (eq_inv_S_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
-  elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
-  @(ex3_2_intro … s1 (s2●𝗦◗r2)) //
-  <unwind2_path_append_ppc_dx //
-  <unwind2_path_S_sn <Hr2 -Hr2 //
-]
-qed-.
-
-(* Inversions with path_lcons ***********************************************)
-
-lemma eq_inv_d_sn_unwind2_path (f) (q) (p) (k):
-      (𝗱k◗q) = ▼[f]p →
-      ∃∃r,h. 𝐞 = ⊗r & ▶[f]r＠⧣❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
-#f * [| #l #q ] #p #k
-[ <list_cons_comm #H0
-  elim (eq_inv_d_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #H1 #H2 destruct
-  /2 width=5 by ex4_2_intro/
-| >list_cons_comm #H0
-  elim (unwind2_path_inv_append_ppc_dx … H0) -H0 // #r1 #r2 #Hr1 #_ #_ -r2
-  elim (eq_inv_d_dx_structure … Hr1)
-]
-qed-.
-
-lemma eq_inv_m_sn_unwind2_path (f) (q) (p):
-      (𝗺◗q) = ▼[f]p → ⊥.
-#f #q #p
->list_cons_comm #H0
-elim (unwind2_path_des_append_pic_sn … H0) <list_cons_comm in H0; //
-#H0 #r1 #r2 #Hr1 #H1 #H2 destruct
-elim (eq_inv_m_dx_structure … Hr1)
-qed-.
-
-lemma eq_inv_L_sn_unwind2_path (f) (q) (p):
-      (𝗟◗q) = ▼[f]p →
-      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[⫯▶[f]r1]r2 & r1●𝗟◗r2 = p.
-#f #q #p
->list_cons_comm #H0
-elim (unwind2_path_des_append_pic_sn … H0) <list_cons_comm in H0; //
-#H0 #r1 #r2 #Hr1 #H1 #H2 destruct
-elim (eq_inv_L_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
-<list_append_assoc in H0; <list_append_assoc
-<unwind2_path_append_ppc_dx //
-<unwind2_path_L_sn <H1 <list_append_empty_dx #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
-/2 width=5 by ex3_2_intro/
-qed-.
-
-lemma eq_inv_A_sn_unwind2_path (f) (q) (p):
-      (𝗔◗q) = ▼[f]p →
-      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▶[f]r1]r2 & r1●𝗔◗r2 = p.
-#f #q #p
->list_cons_comm #H0
-elim (unwind2_path_des_append_pic_sn … H0) <list_cons_comm in H0; //
-#H0 #r1 #r2 #Hr1 #H1 #H2 destruct
-elim (eq_inv_A_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
-<list_append_assoc in H0; <list_append_assoc
-<unwind2_path_append_ppc_dx //
-<unwind2_path_A_sn <H1 <list_append_empty_dx #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
-/2 width=5 by ex3_2_intro/
-qed-.
-
-lemma eq_inv_S_sn_unwind2_path (f) (q) (p):
-      (𝗦◗q) = ▼[f]p →
-      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▶[f]r1]r2 & r1●𝗦◗r2 = p.
-#f #q #p
->list_cons_comm #H0
-elim (unwind2_path_des_append_pic_sn … H0) <list_cons_comm in H0; //
-#H0 #r1 #r2 #Hr1 #H1 #H2 destruct
-elim (eq_inv_S_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
-<list_append_assoc in H0; <list_append_assoc
-<unwind2_path_append_ppc_dx //
-<unwind2_path_S_sn <H1 <list_append_empty_dx #H0
-elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
-/2 width=5 by ex3_2_intro/
-qed-.
-
-(* Advanced eliminations with path ******************************************)
-
-lemma path_ind_unwind (Q:predicate …):
-      Q (𝐞) →
-      (∀k. Q (𝐞) → Q (𝗱k◗𝐞)) →
-      (∀k,l,p. Q (l◗p) → Q (𝗱k◗l◗p)) →
-      (∀p. Q p → Q (𝗺◗p)) →
-      (∀p. Q p → Q (𝗟◗p)) →
-      (∀p. Q p → Q (𝗔◗p)) →
-      (∀p. Q p → Q (𝗦◗p)) →
-      ∀p. Q p.
-#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #p
-@(list_ind_rcons … p) -p // #p * [ #k ]
-[ @(list_ind_rcons … p) -p ]
-/2 width=1 by/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_eq.ma
deleted file mode 100644
index c1b188b60..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_eq.ma
+++ /dev/null
@@ -1,29 +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 "delayed_updating/unwind/unwind2_path.ma".
-include "delayed_updating/unwind/unwind2_rmap_eq.ma".
-
-(* TAILED UNWIND FOR PATH ***************************************************)
-
-(* Constructions with tr_map_eq *********************************************)
-
-lemma unwind2_path_eq_repl (p):
-      stream_eq_repl … (λf1,f2. ▼[f1]p = ▼[f2]p).
-* // * [ #k ] #p #f1 #f2 #Hf //
-<unwind2_path_d_dx <unwind2_path_d_dx
-lapply (unwind2_rmap_eq_repl … Hf) -Hf
-[| #Hf <(tr_pap_eq_repl … Hf) -f2 ] //
-qed-.
-
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma
deleted file mode 100644
index 140dd6f8a..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma
+++ /dev/null
@@ -1,42 +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 "delayed_updating/unwind/unwind2_path.ma".
-include "delayed_updating/unwind/unwind2_rmap_lift.ma".
-include "delayed_updating/substitution/lift_path_structure.ma".
-
-(* TAILED UNWIND FOR PATH ***************************************************)
-
-(* Constructions with lift_path *********************************************)
-
-lemma lift_unwind2_path_after (g) (f) (p):
-      🠡[g]▼[f]p = ▼[g∘f]p.
-#g #f * // * [ #k ] #p //
-<unwind2_path_d_dx <unwind2_path_d_dx <lift_path_d_dx
-<lift_path_structure >tr_compose_pap
-/4 width=1 by tr_pap_eq_repl, eq_f2, eq_f/
-qed.
-
-lemma unwind2_lift_path_after (g) (f) (p):
-      ▼[g]🠡[f]p = ▼[g∘f]p.
-#g #f * // * [ #k ] #p
-[ <unwind2_path_d_dx <unwind2_path_d_dx
-  <structure_lift_path >tr_compose_pap
-  /4 width=1 by tr_pap_eq_repl, eq_f2, eq_f/
-| <unwind2_path_m_dx <unwind2_path_m_dx //
-| <unwind2_path_L_dx <unwind2_path_L_dx //
-| <unwind2_path_A_dx <unwind2_path_A_dx //
-| <unwind2_path_S_dx <unwind2_path_S_dx //
-]
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_eq.ma
deleted file mode 100644
index a78d4b9ed..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_eq.ma
+++ /dev/null
@@ -1,67 +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 "delayed_updating/unwind/unwind2_prototerm.ma".
-include "delayed_updating/unwind/unwind2_path_append.ma".
-include "delayed_updating/syntax/preterm.ma".
-include "delayed_updating/syntax/path_structure_inner.ma".
-include "ground/lib/subset_equivalence.ma".
-
-(* TAILED UNWIND FOR PRETERM ************************************************)
-
-(* Constructions with subset_equivalence ************************************)
-
-lemma unwind2_term_grafted_sn (f) (t) (p): p ϵ 𝐈 →
-      ▼[▶[f]p](t⋔p) ⊆ (▼[f]t)⋔(⊗p).
-#f #t #p #Hp #q * #r #Hr #H0 destruct
-@(ex2_intro … Hr) -Hr
-<unwind2_path_append_pic_sn //
-qed-.
-
-lemma unwind2_term_grafted_dx (f) (t) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
-      (▼[f]t)⋔(⊗p) ⊆ ▼[▶[f]p](t⋔p).
-#f #t #p #H1p #H2p #Ht #q * #r #Hr #H0
-elim (unwind2_path_des_append_pic_sn … (sym_eq … H0)) -H0 //
-#p0 #q0 #Hp0 #Hq0 #H0 destruct
->(Ht … Hp0) [|*: /2 width=2 by ex_intro/ ] -p
-/2 width=1 by in_comp_unwind2_path_term/
-qed-.
-
-lemma unwind2_term_grafted (f) (t) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
-      ▼[▶[f]p](t⋔p) ⇔ (▼[f]t)⋔(⊗p).
-/3 width=1 by unwind2_term_grafted_sn, unwind2_term_grafted_dx, conj/ qed.
-
-lemma unwind2_term_grafted_S_dx (f) (t) (p): p ϵ ▵t → t ϵ 𝐓 →
-      (▼[f]t)⋔((⊗p)◖𝗦) ⊆ ▼[▶[f]p](t⋔(p◖𝗦)).
-#f #t #p #Hp #Ht #q * #r #Hr
->list_append_rcons_sn #H0
-elim (unwind2_path_inv_append_ppc_dx … (sym_eq … H0)) -H0 //
-#p0 #q0 #Hp0 #Hq0 #H0 destruct
->(Ht … Hp0) [|*: /2 width=2 by ex_intro/ ] -p
-elim (eq_inv_S_sn_unwind2_path … Hq0) -Hq0
-#r1 #r2 #Hr1 #Hr2 #H0 destruct
-lapply (preterm_in_root_append_inv_structure_empty_dx … p0 … Ht Hr1)
-[ /2 width=2 by ex_intro/ ] -Hr1 #Hr1 destruct
-/2 width=1 by in_comp_unwind2_path_term/
-qed-.
-
-lemma unwind2_term_grafted_S (f) (t) (p): p ϵ ▵t → t ϵ 𝐓 →
-      ▼[▶[f]p](t⋔(p◖𝗦)) ⇔ (▼[f]t)⋔((⊗p)◖𝗦).
-#f #t #p #Hp #Ht
-@conj
-[ >unwind2_rmap_S_dx >structure_S_dx
-  @unwind2_term_grafted_sn // (**) (* auto fails *)
-| /2 width=1 by unwind2_term_grafted_S_dx/
-]
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma
deleted file mode 100644
index ecf0eaf0f..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma
+++ /dev/null
@@ -1,101 +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 "delayed_updating/unwind/unwind2_prototerm_eq.ma".
-include "delayed_updating/unwind/unwind2_path_append.ma".
-include "delayed_updating/substitution/fsubst.ma".
-include "delayed_updating/syntax/preterm.ma".
-include "delayed_updating/syntax/prototerm_proper.ma".
-
-(* TAILED UNWIND FOR PRETERM ************************************************)
-
-(* Constructions with fsubst and pic ****************************************)
-
-lemma unwind2_term_fsubst_pic_sn (f) (t) (u) (p): p ϵ 𝐈 →
-      (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u] ⊆ ▼[f](t[⋔p←u]).
-#f #t #u #p #Hp #ql * *
-[ #rl * #r #Hr #H1 #H2 destruct
-  >unwind2_path_append_pic_sn
-  /4 width=3 by in_comp_unwind2_path_term, or_introl, ex2_intro/
-| * #q #Hq #H1 #H0
-  @(ex2_intro … H1) @or_intror @conj // *
-  [ <list_append_empty_sn #H2 destruct
-    elim (unwind2_path_root f q) #r #_ #Hr /2 width=2 by/
-  | #l #r #H2 destruct
-    /3 width=2 by unwind2_path_append_pic_sn/
-  ]
-]
-qed-.
-
-lemma unwind2_term_fsubst_pic_dx (f) (t) (u) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
-      ▼[f](t[⋔p←u]) ⊆ (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u].
-#f #t #u #p #Hp #H1p #H2p #ql * #q * *
-[ #r #Hu #H1 #H2 destruct
-  /5 width=3 by unwind2_path_append_pic_sn, ex2_intro, or_introl/
-| #Hq #H0 #H1 destruct
-  @or_intror @conj [ /2 width=1 by in_comp_unwind2_path_term/ ] *
-  [ <list_append_empty_sn #Hr @(H0 … (𝐞)) -H0
-    <list_append_empty_sn @H2p -H2p
-    /2 width=2 by unwind2_path_des_structure, prototerm_in_comp_root/
-  | #l #r #Hr
-    elim (unwind2_path_inv_append_ppc_dx … Hr) -Hr // #s1 #s2 #Hs1 #_ #H1 destruct
-    lapply (H2p … Hs1) -H2p -Hs1 /2 width=2 by ex_intro/
-  ]
-]
-qed-.
-
-lemma unwind2_term_fsubst_pic (f) (t) (u) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
-      (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u] ⇔ ▼[f](t[⋔p←u]).
-/4 width=3 by unwind2_term_fsubst_pic_sn, conj, unwind2_term_fsubst_pic_dx/ qed.
-
-(* Constructions with fsubst and ppc ****************************************)
-
-lemma unwind2_term_fsubst_ppc_sn (f) (t) (u) (p): u ϵ 𝐏 →
-      (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u] ⊆ ▼[f](t[⋔p←u]).
-#f #t #u #p #Hu #ql * *
-[ #rl * #r #Hr #H1 #H2 destruct
-  >unwind2_path_append_ppc_dx
-  /4 width=5 by in_comp_unwind2_path_term, in_comp_tpc_trans, or_introl, ex2_intro/
-| * #q #Hq #H1 #H0
-  @(ex2_intro … H1) @or_intror @conj // *
-  [ <list_append_empty_sn #H2 destruct
-    elim (unwind2_path_root f q) #r #_ #Hr /2 width=2 by/
-  | #l #r #H2 destruct
-    @H0 -H0 [| <unwind2_path_append_ppc_dx /2 width=3 by ppc_rcons/ ]
-  ]
-]
-qed-.
-
-lemma unwind2_term_fsubst_ppc_dx (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 𝐓 →
-      ▼[f](t[⋔p←u]) ⊆ (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u].
-#f #t #u #p #Hu #H1p #H2p #ql * #q * *
-[ #r #Hu #H1 #H2 destruct
-  @or_introl @ex2_intro
-  [|| <unwind2_path_append_ppc_dx /2 width=5 by in_comp_tpc_trans/ ]
-  /2 width=3 by ex2_intro/
-| #Hq #H0 #H1 destruct
-  @or_intror @conj [ /2 width=1 by in_comp_unwind2_path_term/ ] *
-  [ <list_append_empty_sn #Hr @(H0 … (𝐞)) -H0
-    <list_append_empty_sn @H2p -H2p
-    /2 width=2 by unwind2_path_des_structure, prototerm_in_comp_root/
-  | #l #r #Hr
-    elim (unwind2_path_inv_append_ppc_dx … Hr) -Hr // #s1 #s2 #Hs1 #_ #H1 destruct
-    lapply (H2p … Hs1) -H2p -Hs1 /2 width=2 by ex_intro/
-  ]
-]
-qed-.
-
-lemma unwind2_term_fsubst_ppc (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 𝐓 →
-      (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u] ⇔ ▼[f](t[⋔p←u]).
-/4 width=3 by unwind2_term_fsubst_ppc_sn, conj, unwind2_term_fsubst_ppc_dx/ qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm.ma
deleted file mode 100644
index e4e480c66..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm.ma
+++ /dev/null
@@ -1,30 +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 "delayed_updating/unwind/unwind2_path.ma".
-include "delayed_updating/syntax/prototerm.ma".
-include "ground/lib/subset_ext.ma".
-
-(* TAILED UNWIND FOR PROTOTERM **********************************************)
-
-interpretation
-  "unwind (prototerm)"
-  'BlackDownTriangle f t = (subset_ext_f1 ? ? (unwind2_path f) t).
-
-(* Basic constructions ******************************************************)
-
-lemma in_comp_unwind2_path_term (f) (p) (t):
-      p ϵ t → ▼[f]p ϵ ▼[f]t.
-/2 width=1 by subset_in_ext_f1_dx/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_after.ma
deleted file mode 100644
index 9e7dd82f2..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_after.ma
+++ /dev/null
@@ -1,29 +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 "delayed_updating/unwind/unwind2_prototerm_eq.ma".
-include "delayed_updating/unwind/unwind2_path_after.ma".
-
-(* TAILED UNWIND FOR PROTOTERM **********************************************)
-
-(* Constructions with tr_after **********************************************)
-
-lemma unwind2_term_after (f1) (f2) (t):
-      ▼[f2]▼[f1]t ⇔ ▼[f2∘f1]t.
-#f1 #f2 #t @subset_eq_trans
-[
-| @subset_inclusion_ext_f1_compose
-| @subset_equivalence_ext_f1_exteq /2 width=5/
-]
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_constructors.ma
deleted file mode 100644
index 6e3c96fe7..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_constructors.ma
+++ /dev/null
@@ -1,62 +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 "delayed_updating/unwind/unwind2_prototerm_eq.ma".
-include "delayed_updating/unwind/unwind2_path_append.ma".
-include "delayed_updating/syntax/prototerm_constructors.ma".
-
-(* TAILED UNWIND FOR PROTOTERM **********************************************)
-
-(* Constructions with constructors for prototerm ****************************)
-
-lemma unwind2_term_oref_pap (f) (k):
-      (⧣(f＠⧣❨k❩)) ⇔ ▼[f]⧣k.
-#f #k @conj #p *
-[ /2 width=1 by in_comp_unwind2_path_term/
-| #q * #H0 destruct //
-]
-qed.
-
-lemma unwind2_term_iref (f) (t) (k:pnat):
-      ▼[f∘𝐮❨k❩]t ⇔ ▼[f](𝛕k.t).
-#f #t #k @conj
-#p * #q #Hq #H0 destruct
-[ @(ex2_intro … (𝗱k◗𝗺◗q))
-  /2 width=1 by in_comp_iref_hd/
-| elim (in_comp_inv_iref … Hq) -Hq #p #Hp #Ht destruct
-  /2 width=1 by in_comp_unwind2_path_term/
-]
-qed.
-
-lemma unwind2_term_abst (f) (t):
-      (𝛌.▼[⫯f]t) ⇔ ▼[f]𝛌.t.
-#f #t @conj #p #Hp
-[ elim (in_comp_inv_abst … Hp) -Hp #q #H1 * #r #Hr #H2 destruct
-  /3 width=1 by in_comp_unwind2_path_term, in_comp_abst_hd/
-| elim Hp -Hp #q #Hq #H0 destruct
-  elim (in_comp_inv_abst … Hq) -Hq #r #H0 #Hr destruct
-  /3 width=1 by in_comp_unwind2_path_term, in_comp_abst_hd/
-]
-qed.
-
-lemma unwind2_term_appl (f) (v) (t):
-      ＠▼[f]v.▼[f]t ⇔ ▼[f]＠v.t.
-#f #v #t @conj #p #Hp
-[ elim (in_comp_inv_appl … Hp) -Hp * #q #H1 * #r #Hr #H2 destruct
-  /3 width=1 by in_comp_unwind2_path_term, in_comp_appl_sd, in_comp_appl_hd/
-| elim Hp -Hp #q #Hq #H0 destruct
-  elim (in_comp_inv_appl … Hq) -Hq * #r #H0 #Hr destruct
-  /3 width=1 by in_comp_unwind2_path_term, in_comp_appl_sd, in_comp_appl_hd/
-]
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_eq.ma
deleted file mode 100644
index 24e3c7086..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_eq.ma
+++ /dev/null
@@ -1,32 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(**) (* reverse include *)
-include "ground/lib/subset_ext_equivalence.ma".
-include "delayed_updating/unwind/unwind2_path_eq.ma".
-include "delayed_updating/unwind/unwind2_prototerm.ma".
-
-(* TAILED UNWIND FOR PROTOTERM **********************************************)
-
-(* Constructions with subset_equivalence ************************************)
-
-lemma unwind2_term_eq_repl_sn (f1) (f2) (t):
-      f1 ≗ f2 → ▼[f1]t ⇔ ▼[f2]t.
-/3 width=1 by subset_equivalence_ext_f1_exteq, unwind2_path_eq_repl/
-qed.
-
-lemma unwind2_term_eq_repl_dx (f) (t1) (t2):
-      t1 ⇔ t2 → ▼[f]t1 ⇔ ▼[f]t2.
-/2 width=1 by subset_equivalence_ext_f1_bi/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma
deleted file mode 100644
index 6ad293f09..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma
+++ /dev/null
@@ -1,28 +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 "delayed_updating/unwind/unwind2_prototerm.ma".
-include "delayed_updating/unwind/unwind2_path_append.ma".
-include "ground/lib/subset_overlap.ma".
-
-(* TAILED UNWIND FOR PROTOTERM **********************************************)
-
-(* Destructions with pic ****************************************************)
-
-lemma unwind2_term_des_pic (f) (t):
-      ▼[f]t ≬ 𝐈 → t ≬ 𝐈.
-#f #t * #p * #q #Hq #H0 #Hp destruct
-@(subset_ol_i … Hq) -Hq (**) (* auto does not work *)
-@(unwind2_path_des_pic … Hp)
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma
deleted file mode 100644
index 251d7ba72..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma
+++ /dev/null
@@ -1,39 +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                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(**) (* reverse include *)
-include "ground/lib/subset_ext_equivalence.ma".
-include "delayed_updating/substitution/lift_prototerm.ma".
-include "delayed_updating/unwind/unwind2_path_lift.ma".
-include "delayed_updating/unwind/unwind2_prototerm.ma".
-
-(* TAILED UNWIND FOR PROTOTERM **********************************************)
-
-(* Constructions with lift_prototerm ****************************************)
-
-lemma lift_unwind2_term_after (f1) (f2) (t):
-      🠡[f2]▼[f1]t ⇔ ▼[f2∘f1]t.
-#f1 #f2 #t @subset_eq_trans
-[| @subset_inclusion_ext_f1_compose ]
-@subset_equivalence_ext_f1_exteq #p
-@lift_unwind2_path_after
-qed.
-
-lemma unwind2_lift_term_after (f1) (f2) (t):
-      ▼[f2]🠡[f1]t ⇔ ▼[f2∘f1]t.
-#f1 #f2 #t @subset_eq_trans
-[| @subset_inclusion_ext_f1_compose ]
-@subset_equivalence_ext_f1_exteq #p
-@unwind2_lift_path_after
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap.ma
deleted file mode 100644
index 5177fd7ee..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap.ma
+++ /dev/null
@@ -1,92 +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 "delayed_updating/unwind/preunwind2_rmap.ma".
-include "delayed_updating/syntax/path.ma".
-
-(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
-
-rec definition unwind2_rmap (f) (p) on p: tr_map ≝
-match p with
-[ list_empty     ⇒ f
-| list_lcons l q ⇒ ▶[unwind2_rmap f q]l
-].
-
-interpretation
-  "tailed unwind (relocation map)"
-  'BlackRightTriangle f p = (unwind2_rmap f p).
-
-(* Basic constructions ******************************************************)
-
-lemma unwind2_rmap_empty (f):
-      f = ▶[f]𝐞.
-// qed.
-
-lemma unwind2_rmap_rcons (f) (p) (l):
-      ▶[▶[f]p]l = ▶[f](p◖l).
-// qed.
-
-lemma unwind2_rmap_d_dx (f) (p) (k:pnat):
-      ▶[f]p∘𝐮❨k❩ = ▶[f](p◖𝗱k).
-// qed.
-
-lemma unwind2_rmap_m_dx (f) (p):
-      ▶[f]p = ▶[f](p◖𝗺).
-// qed.
-
-lemma unwind2_rmap_L_dx (f) (p):
-      (⫯▶[f]p) = ▶[f](p◖𝗟).
-// qed.
-
-lemma unwind2_rmap_A_dx (f) (p):
-      ▶[f]p = ▶[f](p◖𝗔).
-// qed.
-
-lemma unwind2_rmap_S_dx (f) (p):
-      ▶[f]p = ▶[f](p◖𝗦).
-// qed.
-
-(* Constructions with path_append *******************************************)
-
-lemma unwind2_rmap_append (f) (p) (q):
-      ▶[▶[f]p]q = ▶[f](p●q).
-#f #p #q elim q -q // #l #q #IH
-<unwind2_rmap_rcons <unwind2_rmap_rcons //
-qed.
-
-(* Constructions with path_lcons ********************************************)
-
-lemma unwind2_rmap_lcons (f) (p) (l):
-      ▶[▶[f]l]p = ▶[f](l◗p).
-// qed.
-
-lemma unwind2_rmap_d_sn (f) (p) (k:pnat):
-      ▶[f∘𝐮❨k❩]p = ▶[f](𝗱k◗p).
-// qed.
-
-lemma unwind2_rmap_m_sn (f) (p):
-      ▶[f]p = ▶[f](𝗺◗p).
-// qed.
-
-lemma unwind2_rmap_L_sn (f) (p):
-      ▶[⫯f]p = ▶[f](𝗟◗p).
-// qed.
-
-lemma unwind2_rmap_A_sn (f) (p):
-      ▶[f]p = ▶[f](𝗔◗p).
-// qed.
-
-lemma unwind2_rmap_S_sn (f) (p):
-      ▶[f]p = ▶[f](𝗦◗p).
-// qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_after.ma
deleted file mode 100644
index 7fda762da..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_after.ma
+++ /dev/null
@@ -1,36 +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 "delayed_updating/unwind/unwind2_rmap.ma".
-include "delayed_updating/syntax/path_structure.ma".
-include "ground/relocation/tr_compose_compose.ma".
-include "ground/relocation/tr_compose_pn.ma".
-include "ground/relocation/tr_compose_eq.ma".
-include "ground/relocation/tr_pn_eq.ma".
-include "ground/lib/stream_eq_eq.ma".
-
-(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
-
-(* Constructions with tr_after **********************************************)
-
-lemma unwind2_rmap_after (g) (f) (p:path):
-      ▶[g]⊗p∘▶[f]p ≗ ▶[g∘f]p.
-#g #f #p elim p -p // * [ #k ] #p #IH //
-[ <structure_d_dx <unwind2_rmap_d_dx <unwind2_rmap_d_dx
-  @(stream_eq_canc_sn … (tr_compose_assoc …))
-  /2 width=1 by tr_compose_eq_repl/
-| <structure_L_dx <unwind2_rmap_L_dx <unwind2_rmap_L_dx <unwind2_rmap_L_dx
-  /2 width=1 by tr_push_eq_repl/
-]
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma
deleted file mode 100644
index f38a72ac9..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_closed.ma
+++ /dev/null
@@ -1,101 +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 "delayed_updating/unwind/unwind2_rmap_lift.ma".
-include "delayed_updating/unwind/unwind2_rmap_eq.ma".
-include "delayed_updating/substitution/lift_rmap_structure.ma".
-include "delayed_updating/syntax/path_closed.ma".
-include "delayed_updating/syntax/path_depth.ma".
-include "ground/relocation/nap.ma".
-include "ground/relocation/tr_pushs_tls.ma".
-include "ground/lib/stream_tls_plus.ma".
-include "ground/lib/stream_eq_eq.ma".
-
-(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
-
-(* Destructions with cpp ****************************************************)
-
-lemma nap_plus_unwind2_rmap_closed (o) (e) (f) (q) (m) (n):
-      q ϵ 𝐂❨o,n,e❩ →
-      f＠§❨m+e❩+♭q = ▶[f]q＠§❨m+n❩.
-#o #e #f #q #m #n #Hq elim Hq -q -n //
-#q #n [ #k #_ ] #_ #IH
-[ <depth_d_dx <unwind2_rmap_d_dx
-  <tr_compose_nap <tr_uni_nap //
-| <depth_L_dx <unwind2_rmap_L_dx
-  <tr_nap_push <nplus_succ_dx //
-]
-qed-.
-
-lemma nap_unwind2_rmap_closed (o) (f) (q) (n):
-      q ϵ 𝐂❨o,n,𝟎❩ →
-      f＠§❨𝟎❩+♭q = ▶[f]q＠§❨n❩.
-#o #f #q #n #Hn
-/2 width=2 by nap_plus_unwind2_rmap_closed/
-qed-.
-
-lemma nap_plus_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (m) (n):
-      q ϵ 𝐂❨o,n,𝟎❩ →
-      (⫯▶[f]p)＠§❨m❩+♭q = ▶[f](p●𝗟◗q)＠§❨m+n❩.
-#o #f #p #q #m #n #Hn
-/2 width=2 by nap_plus_unwind2_rmap_closed/
-qed-.
-
-lemma nap_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
-      q ϵ 𝐂❨o,n,𝟎❩ →
-      ♭q = ▶[f](p●𝗟◗q)＠§❨n❩.
-#o #f #p #q #n #Hn
->(nplus_zero_sn n)
-<(nap_plus_unwind2_rmap_append_closed_Lq_dx … Hn) -Hn
-<nplus_zero_sn //
-qed-.
-
-lemma tls_succ_plus_unwind2_rmap_push_closed (o) (f) (q) (n):
-      q ϵ 𝐂❨o,n,𝟎❩ →
-      ∀m. ⇂*[m]f ≗ ⇂*[↑(m+n)]▶[⫯f]q.
-#o #f #q #n #Hn elim Hn -q -n //
-#q #n #k #_ #_ #IH #m
-@(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
->nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold //
-qed-.
-
-lemma tls_succ_unwind2_rmap_push_closed (o) (f) (q) (n):
-      q ϵ 𝐂❨o,n,𝟎❩ →
-      f ≗ ⇂*[↑n]▶[⫯f]q.
-#o #f #q #n #Hn
-/2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
-qed-.
-
-lemma tls_succ_plus_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
-      q ϵ 𝐂❨o,n,𝟎❩ →
-      ∀m. ⇂*[m]▶[f]p ≗ ⇂*[↑(m+n)]▶[f](p●𝗟◗q).
-#o #f #p #q #n #Hn #m
-/2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
-qed-.
-
-lemma tls_succ_unwind2_rmap_closed (f) (q) (n):
-      q ϵ 𝐂❨Ⓕ,n,𝟎❩ →
-      ⇂f ≗ ⇂*[↑n]▶[f]q.
-#f #q #n #Hn
-@(stream_eq_canc_dx … (stream_tls_eq_repl …))
-[| @(unwind2_rmap_eq_repl … (tr_compose_id_dx …)) | skip ]
-@(stream_eq_trans … (stream_tls_eq_repl …))
-[| @(lift_unwind2_rmap_after … ) | skip ]
-<tr_compose_tls <tr_id_unfold
-@(stream_eq_trans … (tr_compose_eq_repl …))
-[| @(tls_succ_unwind2_rmap_push_closed … Hn) | skip | // | skip ]
-@(stream_eq_trans ????? (tr_compose_id_dx …))
-<tr_pap_succ_nap <(nap_unwind2_rmap_closed … Hn) <nplus_zero_sn
-<lift_rmap_structure <stream_tls_succ <tr_tls_pushs //
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma
deleted file mode 100644
index a5127cc45..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_crux.ma
+++ /dev/null
@@ -1,43 +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 "delayed_updating/unwind/unwind2_rmap_closed.ma".
-
-(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
-
-(* Crucial constructions with tr_uni ****************************************)
-
-(* Note: crux of the commutation between unwind and balanced focused reduction *)
-lemma unwind2_rmap_uni_crux (f) (p) (b) (q) (m) (n):
-      b ϵ 𝐂❨Ⓕ,m,𝟎❩ → q ϵ 𝐂❨Ⓕ,n,𝟎❩ →
-      (𝐮❨↑(♭b+♭q)❩ ∘ ▶[f]p ≗ ▶[f](p●𝗔◗b●𝗟◗q) ∘ 𝐮❨↑(m+n)❩).
-#f #p #b #q #m #n #Hm #Hn
-<list_append_rcons_sn <list_append_rcons_sn >list_append_assoc
->list_append_rcons_sn >(list_append_rcons_sn … b)
-@(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
-@(stream_eq_trans ????? (tr_compose_eq_repl …))
-[| @tls_succ_plus_unwind2_rmap_append_closed_Lq_dx // | skip
-|  <nap_plus_unwind2_rmap_append_closed_Lq_dx // | skip
-] -Hn
-@tr_eq_inv_nap_zero_tl_bi
-[ <tr_compose_nap <tr_compose_nap <tr_uni_nap <tr_uni_nap
-  >nsucc_unfold >nplus_succ_dx >nplus_succ_dx <nplus_assoc <nplus_assoc
-  >tr_nap_plus_dx <unwind2_rmap_append <nap_plus_unwind2_rmap_closed
-  /2 width=4 by pcc_A_sn/
-| @(stream_eq_canc_sn … (tr_tl_compose_uni_sn …))
-  @(stream_eq_trans ????? (tr_tl_compose_uni_sn …))
-  >stream_tls_succ <unwind2_rmap_append
-  /3 width=2 by tls_succ_unwind2_rmap_closed, pcc_A_sn/
-]
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_depth.ma
deleted file mode 100644
index cb806673d..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_depth.ma
+++ /dev/null
@@ -1,58 +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 "delayed_updating/unwind/unwind2_path_append.ma".
-include "delayed_updating/syntax/path_depth.ma".
-include "ground/relocation/tr_id_compose.ma".
-include "ground/relocation/tr_compose_compose.ma".
-include "ground/relocation/tr_compose_eq.ma".
-include "ground/relocation/xap.ma".
-include "ground/lib/stream_eq_eq.ma".
-
-(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
-
-(* Constructions with depth *************************************************)
-
-lemma unwind2_rmap_decompose (p) (f):
-      ▶[f]p ≗ (⫯*[♭p]f)∘(▶[𝐢]p).
-#p elim p -p
-[ #f <unwind2_rmap_empty <unwind2_rmap_empty <tr_pushs_zero //
-| * [ #k ] #p #IH #f //
-  [ <unwind2_rmap_d_dx <unwind2_rmap_d_dx <depth_d_dx
-    @(stream_eq_trans … (tr_compose_assoc …))
-    /2 width=1 by tr_compose_eq_repl/
-  | <unwind2_rmap_L_dx <unwind2_rmap_L_dx <depth_L_dx
-    <tr_pushs_succ <tr_compose_push_bi
-    /2 width=1 by tr_push_eq_repl/
-  ]
-]
-qed.
-
-lemma unwind2_rmap_pap_le (f) (p) (h):
-      ▶[𝐢]p＠⧣❨h❩ < ↑♭p → ▶[𝐢]p＠⧣❨h❩ = ▶[f]p＠⧣❨h❩.
-#f #p #h #Hh
->(tr_pap_eq_repl … (▶[f]p) … (unwind2_rmap_decompose …))
-<tr_compose_pap <tr_pap_pushs_le //
-qed.
-
-lemma unwind2_rmap_xap_le (f) (p) (n):
-      ▶[𝐢]p＠❨n❩ ≤ ♭p → ▶[𝐢]p＠❨n❩ = ▶[f]p＠❨n❩.
-(*
-#f #p * // #h <tr_xap_ninj #Hh
->unwind2_rmap_pap_le
-*)
-#f #p #n #Hn
->(tr_xap_eq_repl … (▶[f]p) … (unwind2_rmap_decompose …))
-<tr_compose_xap <tr_xap_pushs_le //
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
deleted file mode 100644
index b93aabf0f..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
+++ /dev/null
@@ -1,36 +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 "delayed_updating/unwind/unwind2_rmap.ma".
-include "delayed_updating/unwind/preunwind2_rmap_eq.ma".
-include "ground/relocation/tr_uni_compose.ma".
-include "ground/arith/nat_rplus_pplus.ma".
-
-(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
-
-(* Constructions with tr_map_eq *********************************************)
-
-lemma unwind2_rmap_eq_repl (p):
-      stream_eq_repl … (λf1,f2. ▶[f1]p ≗ ▶[f2]p).
-#p elim p -p //
-#l #p #IH #f1 #f2 #Hf
-/3 width=1 by preunwind2_rmap_eq_repl/
-qed-.
-
-lemma tls_unwind2_rmap_d_dx (f) (p) (h) (k):
-      ⇂*[h+k]▶[f]p ≗ ⇂*[h]▶[f](p◖𝗱k).
-#f #p #h #k
-<unwind2_rmap_d_dx >nrplus_inj_dx
-/2 width=1 by tr_tls_compose_uni_dx/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_lift.ma
deleted file mode 100644
index b42274ef8..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_lift.ma
+++ /dev/null
@@ -1,43 +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 "delayed_updating/unwind/unwind2_rmap.ma".
-include "delayed_updating/unwind/preunwind2_rmap_lift.ma".
-include "delayed_updating/unwind/preunwind2_rmap_eq.ma".
-include "delayed_updating/substitution/lift_path.ma".
-include "delayed_updating/syntax/path_structure.ma".
-
-(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
-
-(* Constructions with lift_path *********************************************)
-
-lemma lift_unwind2_rmap_after (g) (f) (p):
-      🠢[g]⊗p∘▶[f]p ≗ ▶[g∘f]p.
-#g #f #p elim p -p //
-* [ #k ] #p #IH //
-[ <unwind2_rmap_d_dx <unwind2_rmap_d_dx
-  @(stream_eq_canc_sn … (tr_compose_assoc …))
-  /2 width=1 by tr_compose_eq_repl/
-| <unwind2_rmap_L_dx <unwind2_rmap_L_dx <lift_rmap_L_dx
-  /2 width=1 by tr_push_eq_repl/
-]
-qed.
-
-lemma unwind2_lift_rmap_after (g) (f) (p:path):
-      ▶[g]🠡[f]p∘🠢[f]p ≗ ▶[g∘f]p.
-#g #f #p elim p -p // #l #p #IH
-<lift_path_rcons <lift_rmap_rcons <unwind2_rmap_rcons <unwind2_rmap_rcons
-@(stream_eq_trans … (preunwind2_lift_rmap_after …))
-/2 width=1 by preunwind2_rmap_eq_repl/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_structure.ma
deleted file mode 100644
index 0d949e3b5..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_structure.ma
+++ /dev/null
@@ -1,32 +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 "delayed_updating/unwind/unwind2_rmap.ma".
-include "delayed_updating/syntax/path_structure.ma".
-include "delayed_updating/syntax/path_depth.ma".
-include "ground/relocation/tr_pushs.ma".
-
-(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
-
-(* Constructions with structure and depth ***********************************)
-
-lemma unwind2_rmap_structure (f) (p):
-      (⫯*[♭p]f) = ▶[f]⊗p.
-#f #p elim p -p //
-* [ #k ] #p #IH //
-[ <unwind2_rmap_L_dx //
-| <unwind2_rmap_A_dx //
-| <unwind2_rmap_S_dx //
-]
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/preunwind2_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/preunwind2_rmap.ma
new file mode 100644
index 000000000..d6cdbce3d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/preunwind2_rmap.ma
@@ -0,0 +1,55 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/syntax/label.ma".
+include "delayed_updating/notation/functions/black_righttriangle_2.ma".
+include "ground/relocation/tr_uni.ma".
+include "ground/relocation/tr_compose.ma".
+
+(* TAILED PREUNWIND FOR RELOCATION MAP **************************************)
+
+definition preunwind2_rmap (f) (l): tr_map ≝
+match l with
+[ label_d k ⇒ f∘𝐮❨k❩
+| label_m   ⇒ f
+| label_L   ⇒ ⫯f
+| label_A   ⇒ f
+| label_S   ⇒ f
+].
+
+interpretation
+  "tailed preunwind (relocation map)"
+  'BlackRightTriangle f l = (preunwind2_rmap f l).
+
+(* Basic constructions ******************************************************)
+
+lemma preunwind2_rmap_d (f) (k:pnat):
+      f∘𝐮❨k❩ = ▶[f]𝗱k.
+// qed.
+
+lemma preunwind2_rmap_m (f):
+      f = ▶[f]𝗺.
+// qed.
+
+lemma preunwind2_rmap_L (f):
+      (⫯f) = ▶[f]𝗟.
+// qed.
+
+lemma preunwind2_rmap_A (f):
+      f = ▶[f]𝗔.
+// qed.
+
+lemma preunwind2_rmap_S (f):
+      f = ▶[f]𝗦.
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/preunwind2_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/preunwind2_rmap_eq.ma
new file mode 100644
index 000000000..6c85da3d1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/preunwind2_rmap_eq.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/preunwind2_rmap.ma".
+include "ground/relocation/tr_compose_eq.ma".
+include "ground/relocation/tr_pn_eq.ma".
+
+(* TAILED PREUNWIND FOR RELOCATION MAP **************************************)
+
+(* Constructions with tr_map_eq *********************************************)
+
+lemma preunwind2_rmap_eq_repl (l):
+      stream_eq_repl … (λf1,f2. ▶[f1]l ≗ ▶[f2]l).
+* // #k #f1 #f2 #Hf
+/2 width=1 by tr_compose_eq_repl/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/preunwind2_rmap_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/preunwind2_rmap_lift.ma
new file mode 100644
index 000000000..ff3e3c8aa
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/preunwind2_rmap_lift.ma
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/preunwind2_rmap.ma".
+include "delayed_updating/substitution/prelift_label.ma".
+include "delayed_updating/substitution/prelift_rmap.ma".
+include "ground/relocation/tr_uni_compose.ma".
+include "ground/relocation/tr_compose_compose.ma".
+include "ground/relocation/tr_compose_eq.ma".
+include "ground/lib/stream_eq_eq.ma".
+
+(* TAILED PREUNWIND FOR RELOCATION MAP **************************************)
+
+(* Constructions with lift_path *********************************************)
+
+lemma preunwind2_lift_rmap_after (g) (f) (l):
+      ▶[g]🠡[f]l∘🠢[f]l ≗ ▶[g∘f]l.
+#g #f * // #k
+<prelift_label_d <prelift_rmap_d <preunwind2_rmap_d <preunwind2_rmap_d
+@(stream_eq_trans … (tr_compose_assoc …))
+@(stream_eq_canc_dx … (tr_compose_assoc …))
+/2 width=1 by tr_compose_eq_repl/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path.ma
new file mode 100644
index 000000000..85bc220d9
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path.ma
@@ -0,0 +1,170 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/unwind2_rmap.ma".
+include "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/notation/functions/black_downtriangle_2.ma".
+
+(* TAILED UNWIND FOR PATH ***************************************************)
+
+definition unwind2_path (f) (p): path ≝
+match p with
+[ list_empty     ⇒ (𝐞)
+| list_lcons l q ⇒
+  match l with
+  [ label_d k ⇒ (⊗q)◖𝗱(▶[f]q＠⧣❨k❩)
+  | label_m   ⇒ ⊗p
+  | label_L   ⇒ ⊗p
+  | label_A   ⇒ ⊗p
+  | label_S   ⇒ ⊗p
+  ]
+].
+
+interpretation
+  "tailed unwind (path)"
+  'BlackDownTriangle f p = (unwind2_path f p).
+
+(* Basic constructions ******************************************************)
+
+lemma unwind2_path_empty (f):
+      (𝐞) = ▼[f]𝐞.
+// qed.
+
+lemma unwind2_path_d_dx (f) (p) (k) :
+      (⊗p)◖𝗱((▶[f]p)＠⧣❨k❩) = ▼[f](p◖𝗱k).
+// qed.
+
+lemma unwind2_path_m_dx (f) (p):
+      ⊗p = ▼[f](p◖𝗺).
+// qed.
+
+lemma unwind2_path_L_dx (f) (p):
+      (⊗p)◖𝗟 = ▼[f](p◖𝗟).
+// qed.
+
+lemma unwind2_path_A_dx (f) (p):
+      (⊗p)◖𝗔 = ▼[f](p◖𝗔).
+// qed.
+
+lemma unwind2_path_S_dx (f) (p):
+      (⊗p)◖𝗦 = ▼[f](p◖𝗦).
+// qed.
+
+(* Constructions with structure *********************************************)
+
+lemma structure_unwind2_path (f) (p):
+      ⊗p = ⊗▼[f]p.
+#f * // * [ #k ] #p //
+qed.
+
+lemma unwind2_path_structure (f) (p):
+      ⊗p = ▼[f]⊗p.
+#f #p elim p -p // * [ #k ] #p #IH //
+[ <structure_L_dx <unwind2_path_L_dx //
+| <structure_A_dx <unwind2_path_A_dx //
+| <structure_S_dx <unwind2_path_S_dx //
+]
+qed.
+
+lemma unwind2_path_root (f) (p):
+      ∃∃r. 𝐞 = ⊗r & ⊗p●r = ▼[f]p.
+#f * [| * [ #k ] #p ]
+/2 width=3 by ex2_intro/
+<unwind2_path_d_dx <structure_d_dx
+/2 width=3 by ex2_intro/
+qed-.
+
+(* Destructions with structure **********************************************)
+
+lemma unwind2_path_des_structure (f) (q) (p):
+      ⊗q = ▼[f]p → ⊗q = ⊗p.
+// qed-.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_d_dx_unwind2_path (f) (q) (p) (h):
+      q◖𝗱h = ▼[f]p →
+      ∃∃r,k. q = ⊗r & h = ▶[f]r＠⧣❨k❩ & r◖𝗱k = p.
+#f #q * [| * [ #k ] #p ] #h
+[ <unwind2_path_empty #H0 destruct
+| <unwind2_path_d_dx #H0 destruct
+  /2 width=5 by ex3_2_intro/
+| <unwind2_path_m_dx #H0
+  elim (eq_inv_d_dx_structure … H0)
+| <unwind2_path_L_dx #H0 destruct
+| <unwind2_path_A_dx #H0 destruct
+| <unwind2_path_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_m_dx_unwind2_path (f) (q) (p):
+      q◖𝗺 = ▼[f]p → ⊥.
+#f #q * [| * [ #k ] #p ]
+[ <unwind2_path_empty #H0 destruct
+| <unwind2_path_d_dx #H0 destruct
+| <unwind2_path_m_dx #H0
+  elim (eq_inv_m_dx_structure … H0)
+| <unwind2_path_L_dx #H0 destruct
+| <unwind2_path_A_dx #H0 destruct
+| <unwind2_path_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_L_dx_unwind2_path (f) (q) (p):
+      q◖𝗟 = ▼[f]p →
+      ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗟◗r2 = p.
+#f #q * [| * [ #k ] #p ]
+[ <unwind2_path_empty #H0 destruct
+| <unwind2_path_d_dx #H0 destruct
+| <unwind2_path_m_dx #H0
+  elim (eq_inv_L_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
+  /2 width=5 by ex3_2_intro/
+| <unwind2_path_L_dx #H0 destruct
+  /2 width=5 by ex3_2_intro/
+| <unwind2_path_A_dx #H0 destruct
+| <unwind2_path_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_A_dx_unwind2_path (f) (q) (p):
+      q◖𝗔 = ▼[f]p →
+      ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗔◗r2 = p.
+#f #q * [| * [ #k ] #p ]
+[ <unwind2_path_empty #H0 destruct
+| <unwind2_path_d_dx #H0 destruct
+| <unwind2_path_m_dx #H0
+  elim (eq_inv_A_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
+  /2 width=5 by ex3_2_intro/
+| <unwind2_path_L_dx #H0 destruct
+| <unwind2_path_A_dx #H0 destruct
+  /2 width=5 by ex3_2_intro/
+| <unwind2_path_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_S_dx_unwind2_path (f) (q) (p):
+      q◖𝗦 = ▼[f]p →
+      ∃∃r1,r2. q = ⊗r1 & ∀g. 𝐞 = ▼[g]r2 & r1●𝗦◗r2 = p.
+#f #q * [| * [ #k ] #p ]
+[ <unwind2_path_empty #H0 destruct
+| <unwind2_path_d_dx #H0 destruct
+| <unwind2_path_m_dx #H0
+  elim (eq_inv_S_dx_structure … H0) -H0 #r1 #r2 #H1 #H2 #H3 destruct
+  /2 width=5 by ex3_2_intro/
+| <unwind2_path_L_dx #H0 destruct
+| <unwind2_path_A_dx #H0 destruct
+| <unwind2_path_S_dx #H0 destruct
+  /2 width=5 by ex3_2_intro/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_after.ma
new file mode 100644
index 000000000..955f4b1c8
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_after.ma
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/unwind2_path_eq.ma".
+include "delayed_updating/unwind_k/unwind2_rmap_after.ma".
+
+(* TAILED UNWIND FOR PATH ***************************************************)
+
+(* Properties with tr_after *************************************************)
+
+lemma unwind2_path_after (g) (f) (p):
+      ▼[g]▼[f]p = ▼[g∘f]p.
+#g #f * // * [ #k ] #p //
+<unwind2_path_d_dx <unwind2_path_d_dx
+@eq_f2 // @eq_f >tr_compose_pap
+/2 width=3 by tr_pap_eq_repl/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_append.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_append.ma
new file mode 100644
index 000000000..cdff0a580
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_append.ma
@@ -0,0 +1,244 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/unwind2_path.ma".
+include "delayed_updating/syntax/path_inner.ma".
+include "delayed_updating/syntax/path_proper.ma".
+include "ground/xoa/ex_4_2.ma".
+
+(* TAILED UNWIND FOR PATH ***************************************************)
+
+(* Constructions with pic ***************************************************)
+
+lemma unwind2_path_pic (f) (p):
+      p ϵ 𝐈 → ⊗p = ▼[f]p.
+#f * // * // #k #q #Hq
+elim (pic_inv_d_dx … Hq)
+qed-.
+
+(* Constructions with append and pic ****************************************)
+
+lemma unwind2_path_append_pic_sn (f) (p) (q): p ϵ 𝐈 →
+      (⊗p)●(▼[▶[f]p]q) = ▼[f](p●q).
+#f #p * [ #Hp | * [ #k ] #q #_ ] //
+[ <(unwind2_path_pic … Hp) -Hp //
+| <unwind2_path_d_dx <unwind2_path_d_dx
+  /2 width=3 by trans_eq/
+| <unwind2_path_L_dx <unwind2_path_L_dx //
+| <unwind2_path_A_dx <unwind2_path_A_dx //
+| <unwind2_path_S_dx <unwind2_path_S_dx //
+]
+qed.
+
+(* Constructions with append and ppc ****************************************)
+
+lemma unwind2_path_append_ppc_dx (f) (p) (q): q ϵ 𝐏 →
+      (⊗p)●(▼[▶[f]p]q) = ▼[f](p●q).
+#f #p * [ #Hq | * [ #k ] #q #_ ] //
+[ elim (ppc_inv_empty … Hq)
+| <unwind2_path_d_dx <unwind2_path_d_dx
+  /2 width=3 by trans_eq/
+| <unwind2_path_L_dx <unwind2_path_L_dx //
+| <unwind2_path_A_dx <unwind2_path_A_dx //
+| <unwind2_path_S_dx <unwind2_path_S_dx //
+]
+qed.
+
+(* Constructions with path_lcons ********************************************)
+
+lemma unwind2_path_d_empty (f) (k):
+      (𝗱(f＠⧣❨k❩)◗𝐞) = ▼[f](𝗱k◗𝐞).
+// qed.
+
+lemma unwind2_path_d_lcons (f) (p) (l) (k:pnat):
+      ▼[f∘𝐮❨k❩](l◗p) = ▼[f](𝗱k◗l◗p).
+#f #p #l #k <unwind2_path_append_ppc_dx in ⊢ (???%); //
+qed.
+
+lemma unwind2_path_m_sn (f) (p):
+      ▼[f]p = ▼[f](𝗺◗p).
+#f #p <unwind2_path_append_pic_sn //
+qed.
+
+lemma unwind2_path_L_sn (f) (p):
+      (𝗟◗▼[⫯f]p) = ▼[f](𝗟◗p).
+#f #p <unwind2_path_append_pic_sn //
+qed.
+
+lemma unwind2_path_A_sn (f) (p):
+      (𝗔◗▼[f]p) = ▼[f](𝗔◗p).
+#f #p <unwind2_path_append_pic_sn //
+qed.
+
+lemma unwind2_path_S_sn (f) (p):
+      (𝗦◗▼[f]p) = ▼[f](𝗦◗p).
+#f #p <unwind2_path_append_pic_sn //
+qed.
+
+(* Destructions with pic ****************************************************)
+
+lemma unwind2_path_des_pic (f) (p):
+      ▼[f]p ϵ 𝐈 → p ϵ 𝐈.
+#f * // * [ #k ] #p //
+<unwind2_path_d_dx #H0
+elim (pic_inv_d_dx … H0)
+qed-.
+
+(* Destructions with append and pic *****************************************)
+
+lemma unwind2_path_des_append_pic_sn (f) (p) (q1) (q2):
+      q1 ϵ 𝐈 → q1●q2 = ▼[f]p →
+      ∃∃p1,p2. q1 = ⊗p1 & q2 = ▼[▶[f]p1]p2 & p1●p2 = p.
+#f #p #q1 * [| * [ #k ] #q2 ] #Hq1
+[ <list_append_empty_sn #H0 destruct
+  lapply (unwind2_path_des_pic … Hq1) -Hq1 #Hp
+  <(unwind2_path_pic … Hp) -Hp
+  /2 width=5 by ex3_2_intro/
+| #H0 elim (eq_inv_d_dx_unwind2_path … H0) -H0 #r #h #Hr #H1 #H2 destruct
+  elim (eq_inv_append_structure … Hr) -Hr #s1 #s2 #H1 #H2 #H3 destruct
+  /2 width=5 by ex3_2_intro/
+| #H0 elim (eq_inv_m_dx_unwind2_path … H0)
+| #H0 elim (eq_inv_L_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
+  elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
+  @(ex3_2_intro … s1 (s2●𝗟◗r2)) //
+  <unwind2_path_append_ppc_dx //
+  <unwind2_path_L_sn <Hr2 -Hr2 //
+| #H0 elim (eq_inv_A_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
+  elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
+  @(ex3_2_intro … s1 (s2●𝗔◗r2)) //
+  <unwind2_path_append_ppc_dx //
+  <unwind2_path_A_sn <Hr2 -Hr2 //
+| #H0 elim (eq_inv_S_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
+  elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
+  @(ex3_2_intro … s1 (s2●𝗦◗r2)) //
+  <unwind2_path_append_ppc_dx //
+  <unwind2_path_S_sn <Hr2 -Hr2 //
+]
+qed-.
+
+(* Inversions with append and ppc *******************************************)
+
+lemma unwind2_path_inv_append_ppc_dx (f) (p) (q1) (q2):
+      q2 ϵ 𝐏 → q1●q2 = ▼[f]p →
+      ∃∃p1,p2. q1 = ⊗p1 & q2 = ▼[▶[f]p1]p2 & p1●p2 = p.
+#f #p #q1 * [| * [ #k ] #q2 ] #Hq1
+[ <list_append_empty_sn #H0 destruct
+  elim (ppc_inv_empty … Hq1)
+| #H0 elim (eq_inv_d_dx_unwind2_path … H0) -H0 #r #h #Hr #H1 #H2 destruct
+  elim (eq_inv_append_structure … Hr) -Hr #s1 #s2 #H1 #H2 #H3 destruct
+  /2 width=5 by ex3_2_intro/
+| #H0 elim (eq_inv_m_dx_unwind2_path … H0)
+| #H0 elim (eq_inv_L_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
+  elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
+  @(ex3_2_intro … s1 (s2●𝗟◗r2)) //
+  <unwind2_path_append_ppc_dx //
+  <unwind2_path_L_sn <Hr2 -Hr2 //
+| #H0 elim (eq_inv_A_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
+  elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
+  @(ex3_2_intro … s1 (s2●𝗔◗r2)) //
+  <unwind2_path_append_ppc_dx //
+  <unwind2_path_A_sn <Hr2 -Hr2 //
+| #H0 elim (eq_inv_S_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
+  elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
+  @(ex3_2_intro … s1 (s2●𝗦◗r2)) //
+  <unwind2_path_append_ppc_dx //
+  <unwind2_path_S_sn <Hr2 -Hr2 //
+]
+qed-.
+
+(* Inversions with path_lcons ***********************************************)
+
+lemma eq_inv_d_sn_unwind2_path (f) (q) (p) (k):
+      (𝗱k◗q) = ▼[f]p →
+      ∃∃r,h. 𝐞 = ⊗r & ▶[f]r＠⧣❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
+#f * [| #l #q ] #p #k
+[ <list_cons_comm #H0
+  elim (eq_inv_d_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #H1 #H2 destruct
+  /2 width=5 by ex4_2_intro/
+| >list_cons_comm #H0
+  elim (unwind2_path_inv_append_ppc_dx … H0) -H0 // #r1 #r2 #Hr1 #_ #_ -r2
+  elim (eq_inv_d_dx_structure … Hr1)
+]
+qed-.
+
+lemma eq_inv_m_sn_unwind2_path (f) (q) (p):
+      (𝗺◗q) = ▼[f]p → ⊥.
+#f #q #p
+>list_cons_comm #H0
+elim (unwind2_path_des_append_pic_sn … H0) <list_cons_comm in H0; //
+#H0 #r1 #r2 #Hr1 #H1 #H2 destruct
+elim (eq_inv_m_dx_structure … Hr1)
+qed-.
+
+lemma eq_inv_L_sn_unwind2_path (f) (q) (p):
+      (𝗟◗q) = ▼[f]p →
+      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[⫯▶[f]r1]r2 & r1●𝗟◗r2 = p.
+#f #q #p
+>list_cons_comm #H0
+elim (unwind2_path_des_append_pic_sn … H0) <list_cons_comm in H0; //
+#H0 #r1 #r2 #Hr1 #H1 #H2 destruct
+elim (eq_inv_L_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
+<list_append_assoc in H0; <list_append_assoc
+<unwind2_path_append_ppc_dx //
+<unwind2_path_L_sn <H1 <list_append_empty_dx #H0
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
+/2 width=5 by ex3_2_intro/
+qed-.
+
+lemma eq_inv_A_sn_unwind2_path (f) (q) (p):
+      (𝗔◗q) = ▼[f]p →
+      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▶[f]r1]r2 & r1●𝗔◗r2 = p.
+#f #q #p
+>list_cons_comm #H0
+elim (unwind2_path_des_append_pic_sn … H0) <list_cons_comm in H0; //
+#H0 #r1 #r2 #Hr1 #H1 #H2 destruct
+elim (eq_inv_A_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
+<list_append_assoc in H0; <list_append_assoc
+<unwind2_path_append_ppc_dx //
+<unwind2_path_A_sn <H1 <list_append_empty_dx #H0
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
+/2 width=5 by ex3_2_intro/
+qed-.
+
+lemma eq_inv_S_sn_unwind2_path (f) (q) (p):
+      (𝗦◗q) = ▼[f]p →
+      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▶[f]r1]r2 & r1●𝗦◗r2 = p.
+#f #q #p
+>list_cons_comm #H0
+elim (unwind2_path_des_append_pic_sn … H0) <list_cons_comm in H0; //
+#H0 #r1 #r2 #Hr1 #H1 #H2 destruct
+elim (eq_inv_S_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
+<list_append_assoc in H0; <list_append_assoc
+<unwind2_path_append_ppc_dx //
+<unwind2_path_S_sn <H1 <list_append_empty_dx #H0
+elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
+/2 width=5 by ex3_2_intro/
+qed-.
+
+(* Advanced eliminations with path ******************************************)
+
+lemma path_ind_unwind (Q:predicate …):
+      Q (𝐞) →
+      (∀k. Q (𝐞) → Q (𝗱k◗𝐞)) →
+      (∀k,l,p. Q (l◗p) → Q (𝗱k◗l◗p)) →
+      (∀p. Q p → Q (𝗺◗p)) →
+      (∀p. Q p → Q (𝗟◗p)) →
+      (∀p. Q p → Q (𝗔◗p)) →
+      (∀p. Q p → Q (𝗦◗p)) →
+      ∀p. Q p.
+#Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #p
+@(list_ind_rcons … p) -p // #p * [ #k ]
+[ @(list_ind_rcons … p) -p ]
+/2 width=1 by/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_eq.ma
new file mode 100644
index 000000000..fb44a3fba
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_eq.ma
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/unwind2_path.ma".
+include "delayed_updating/unwind_k/unwind2_rmap_eq.ma".
+
+(* TAILED UNWIND FOR PATH ***************************************************)
+
+(* Constructions with tr_map_eq *********************************************)
+
+lemma unwind2_path_eq_repl (p):
+      stream_eq_repl … (λf1,f2. ▼[f1]p = ▼[f2]p).
+* // * [ #k ] #p #f1 #f2 #Hf //
+<unwind2_path_d_dx <unwind2_path_d_dx
+lapply (unwind2_rmap_eq_repl … Hf) -Hf
+[| #Hf <(tr_pap_eq_repl … Hf) -f2 ] //
+qed-.
+
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_lift.ma
new file mode 100644
index 000000000..abd752471
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_path_lift.ma
@@ -0,0 +1,42 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/unwind2_path.ma".
+include "delayed_updating/unwind_k/unwind2_rmap_lift.ma".
+include "delayed_updating/substitution/lift_path_structure.ma".
+
+(* TAILED UNWIND FOR PATH ***************************************************)
+
+(* Constructions with lift_path *********************************************)
+
+lemma lift_unwind2_path_after (g) (f) (p):
+      🠡[g]▼[f]p = ▼[g∘f]p.
+#g #f * // * [ #k ] #p //
+<unwind2_path_d_dx <unwind2_path_d_dx <lift_path_d_dx
+<lift_path_structure >tr_compose_pap
+/4 width=1 by tr_pap_eq_repl, eq_f2, eq_f/
+qed.
+
+lemma unwind2_lift_path_after (g) (f) (p):
+      ▼[g]🠡[f]p = ▼[g∘f]p.
+#g #f * // * [ #k ] #p
+[ <unwind2_path_d_dx <unwind2_path_d_dx
+  <structure_lift_path >tr_compose_pap
+  /4 width=1 by tr_pap_eq_repl, eq_f2, eq_f/
+| <unwind2_path_m_dx <unwind2_path_m_dx //
+| <unwind2_path_L_dx <unwind2_path_L_dx //
+| <unwind2_path_A_dx <unwind2_path_A_dx //
+| <unwind2_path_S_dx <unwind2_path_S_dx //
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_preterm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_preterm_eq.ma
new file mode 100644
index 000000000..8264293d1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_preterm_eq.ma
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/unwind2_prototerm.ma".
+include "delayed_updating/unwind_k/unwind2_path_append.ma".
+include "delayed_updating/syntax/preterm.ma".
+include "delayed_updating/syntax/path_structure_inner.ma".
+include "ground/lib/subset_equivalence.ma".
+
+(* TAILED UNWIND FOR PRETERM ************************************************)
+
+(* Constructions with subset_equivalence ************************************)
+
+lemma unwind2_term_grafted_sn (f) (t) (p): p ϵ 𝐈 →
+      ▼[▶[f]p](t⋔p) ⊆ (▼[f]t)⋔(⊗p).
+#f #t #p #Hp #q * #r #Hr #H0 destruct
+@(ex2_intro … Hr) -Hr
+<unwind2_path_append_pic_sn //
+qed-.
+
+lemma unwind2_term_grafted_dx (f) (t) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
+      (▼[f]t)⋔(⊗p) ⊆ ▼[▶[f]p](t⋔p).
+#f #t #p #H1p #H2p #Ht #q * #r #Hr #H0
+elim (unwind2_path_des_append_pic_sn … (sym_eq … H0)) -H0 //
+#p0 #q0 #Hp0 #Hq0 #H0 destruct
+>(Ht … Hp0) [|*: /2 width=2 by ex_intro/ ] -p
+/2 width=1 by in_comp_unwind2_path_term/
+qed-.
+
+lemma unwind2_term_grafted (f) (t) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
+      ▼[▶[f]p](t⋔p) ⇔ (▼[f]t)⋔(⊗p).
+/3 width=1 by unwind2_term_grafted_sn, unwind2_term_grafted_dx, conj/ qed.
+
+lemma unwind2_term_grafted_S_dx (f) (t) (p): p ϵ ▵t → t ϵ 𝐓 →
+      (▼[f]t)⋔((⊗p)◖𝗦) ⊆ ▼[▶[f]p](t⋔(p◖𝗦)).
+#f #t #p #Hp #Ht #q * #r #Hr
+>list_append_rcons_sn #H0
+elim (unwind2_path_inv_append_ppc_dx … (sym_eq … H0)) -H0 //
+#p0 #q0 #Hp0 #Hq0 #H0 destruct
+>(Ht … Hp0) [|*: /2 width=2 by ex_intro/ ] -p
+elim (eq_inv_S_sn_unwind2_path … Hq0) -Hq0
+#r1 #r2 #Hr1 #Hr2 #H0 destruct
+lapply (preterm_in_root_append_inv_structure_empty_dx … p0 … Ht Hr1)
+[ /2 width=2 by ex_intro/ ] -Hr1 #Hr1 destruct
+/2 width=1 by in_comp_unwind2_path_term/
+qed-.
+
+lemma unwind2_term_grafted_S (f) (t) (p): p ϵ ▵t → t ϵ 𝐓 →
+      ▼[▶[f]p](t⋔(p◖𝗦)) ⇔ (▼[f]t)⋔((⊗p)◖𝗦).
+#f #t #p #Hp #Ht
+@conj
+[ >unwind2_rmap_S_dx >structure_S_dx
+  @unwind2_term_grafted_sn // (**) (* auto fails *)
+| /2 width=1 by unwind2_term_grafted_S_dx/
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_preterm_fsubst.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_preterm_fsubst.ma
new file mode 100644
index 000000000..708ac32a2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_preterm_fsubst.ma
@@ -0,0 +1,101 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/unwind2_prototerm_eq.ma".
+include "delayed_updating/unwind_k/unwind2_path_append.ma".
+include "delayed_updating/substitution/fsubst.ma".
+include "delayed_updating/syntax/preterm.ma".
+include "delayed_updating/syntax/prototerm_proper.ma".
+
+(* TAILED UNWIND FOR PRETERM ************************************************)
+
+(* Constructions with fsubst and pic ****************************************)
+
+lemma unwind2_term_fsubst_pic_sn (f) (t) (u) (p): p ϵ 𝐈 →
+      (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u] ⊆ ▼[f](t[⋔p←u]).
+#f #t #u #p #Hp #ql * *
+[ #rl * #r #Hr #H1 #H2 destruct
+  >unwind2_path_append_pic_sn
+  /4 width=3 by in_comp_unwind2_path_term, or_introl, ex2_intro/
+| * #q #Hq #H1 #H0
+  @(ex2_intro … H1) @or_intror @conj // *
+  [ <list_append_empty_sn #H2 destruct
+    elim (unwind2_path_root f q) #r #_ #Hr /2 width=2 by/
+  | #l #r #H2 destruct
+    /3 width=2 by unwind2_path_append_pic_sn/
+  ]
+]
+qed-.
+
+lemma unwind2_term_fsubst_pic_dx (f) (t) (u) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
+      ▼[f](t[⋔p←u]) ⊆ (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u].
+#f #t #u #p #Hp #H1p #H2p #ql * #q * *
+[ #r #Hu #H1 #H2 destruct
+  /5 width=3 by unwind2_path_append_pic_sn, ex2_intro, or_introl/
+| #Hq #H0 #H1 destruct
+  @or_intror @conj [ /2 width=1 by in_comp_unwind2_path_term/ ] *
+  [ <list_append_empty_sn #Hr @(H0 … (𝐞)) -H0
+    <list_append_empty_sn @H2p -H2p
+    /2 width=2 by unwind2_path_des_structure, prototerm_in_comp_root/
+  | #l #r #Hr
+    elim (unwind2_path_inv_append_ppc_dx … Hr) -Hr // #s1 #s2 #Hs1 #_ #H1 destruct
+    lapply (H2p … Hs1) -H2p -Hs1 /2 width=2 by ex_intro/
+  ]
+]
+qed-.
+
+lemma unwind2_term_fsubst_pic (f) (t) (u) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
+      (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u] ⇔ ▼[f](t[⋔p←u]).
+/4 width=3 by unwind2_term_fsubst_pic_sn, conj, unwind2_term_fsubst_pic_dx/ qed.
+
+(* Constructions with fsubst and ppc ****************************************)
+
+lemma unwind2_term_fsubst_ppc_sn (f) (t) (u) (p): u ϵ 𝐏 →
+      (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u] ⊆ ▼[f](t[⋔p←u]).
+#f #t #u #p #Hu #ql * *
+[ #rl * #r #Hr #H1 #H2 destruct
+  >unwind2_path_append_ppc_dx
+  /4 width=5 by in_comp_unwind2_path_term, in_comp_tpc_trans, or_introl, ex2_intro/
+| * #q #Hq #H1 #H0
+  @(ex2_intro … H1) @or_intror @conj // *
+  [ <list_append_empty_sn #H2 destruct
+    elim (unwind2_path_root f q) #r #_ #Hr /2 width=2 by/
+  | #l #r #H2 destruct
+    @H0 -H0 [| <unwind2_path_append_ppc_dx /2 width=3 by ppc_rcons/ ]
+  ]
+]
+qed-.
+
+lemma unwind2_term_fsubst_ppc_dx (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 𝐓 →
+      ▼[f](t[⋔p←u]) ⊆ (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u].
+#f #t #u #p #Hu #H1p #H2p #ql * #q * *
+[ #r #Hu #H1 #H2 destruct
+  @or_introl @ex2_intro
+  [|| <unwind2_path_append_ppc_dx /2 width=5 by in_comp_tpc_trans/ ]
+  /2 width=3 by ex2_intro/
+| #Hq #H0 #H1 destruct
+  @or_intror @conj [ /2 width=1 by in_comp_unwind2_path_term/ ] *
+  [ <list_append_empty_sn #Hr @(H0 … (𝐞)) -H0
+    <list_append_empty_sn @H2p -H2p
+    /2 width=2 by unwind2_path_des_structure, prototerm_in_comp_root/
+  | #l #r #Hr
+    elim (unwind2_path_inv_append_ppc_dx … Hr) -Hr // #s1 #s2 #Hs1 #_ #H1 destruct
+    lapply (H2p … Hs1) -H2p -Hs1 /2 width=2 by ex_intro/
+  ]
+]
+qed-.
+
+lemma unwind2_term_fsubst_ppc (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 𝐓 →
+      (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u] ⇔ ▼[f](t[⋔p←u]).
+/4 width=3 by unwind2_term_fsubst_ppc_sn, conj, unwind2_term_fsubst_ppc_dx/ qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm.ma
new file mode 100644
index 000000000..9a21490c4
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm.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 "delayed_updating/unwind_k/unwind2_path.ma".
+include "delayed_updating/syntax/prototerm.ma".
+include "ground/lib/subset_ext.ma".
+
+(* TAILED UNWIND FOR PROTOTERM **********************************************)
+
+interpretation
+  "unwind (prototerm)"
+  'BlackDownTriangle f t = (subset_ext_f1 ? ? (unwind2_path f) t).
+
+(* Basic constructions ******************************************************)
+
+lemma in_comp_unwind2_path_term (f) (p) (t):
+      p ϵ t → ▼[f]p ϵ ▼[f]t.
+/2 width=1 by subset_in_ext_f1_dx/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_after.ma
new file mode 100644
index 000000000..0edc58e1f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_after.ma
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/unwind2_prototerm_eq.ma".
+include "delayed_updating/unwind_k/unwind2_path_after.ma".
+
+(* TAILED UNWIND FOR PROTOTERM **********************************************)
+
+(* Constructions with tr_after **********************************************)
+
+lemma unwind2_term_after (f1) (f2) (t):
+      ▼[f2]▼[f1]t ⇔ ▼[f2∘f1]t.
+#f1 #f2 #t @subset_eq_trans
+[
+| @subset_inclusion_ext_f1_compose
+| @subset_equivalence_ext_f1_exteq /2 width=5/
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_constructors.ma
new file mode 100644
index 000000000..7a6d0ef06
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_constructors.ma
@@ -0,0 +1,62 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/unwind2_prototerm_eq.ma".
+include "delayed_updating/unwind_k/unwind2_path_append.ma".
+include "delayed_updating/syntax/prototerm_constructors.ma".
+
+(* TAILED UNWIND FOR PROTOTERM **********************************************)
+
+(* Constructions with constructors for prototerm ****************************)
+
+lemma unwind2_term_oref_pap (f) (k):
+      (⧣(f＠⧣❨k❩)) ⇔ ▼[f]⧣k.
+#f #k @conj #p *
+[ /2 width=1 by in_comp_unwind2_path_term/
+| #q * #H0 destruct //
+]
+qed.
+
+lemma unwind2_term_iref (f) (t) (k:pnat):
+      ▼[f∘𝐮❨k❩]t ⇔ ▼[f](𝛕k.t).
+#f #t #k @conj
+#p * #q #Hq #H0 destruct
+[ @(ex2_intro … (𝗱k◗𝗺◗q))
+  /2 width=1 by in_comp_iref_hd/
+| elim (in_comp_inv_iref … Hq) -Hq #p #Hp #Ht destruct
+  /2 width=1 by in_comp_unwind2_path_term/
+]
+qed.
+
+lemma unwind2_term_abst (f) (t):
+      (𝛌.▼[⫯f]t) ⇔ ▼[f]𝛌.t.
+#f #t @conj #p #Hp
+[ elim (in_comp_inv_abst … Hp) -Hp #q #H1 * #r #Hr #H2 destruct
+  /3 width=1 by in_comp_unwind2_path_term, in_comp_abst_hd/
+| elim Hp -Hp #q #Hq #H0 destruct
+  elim (in_comp_inv_abst … Hq) -Hq #r #H0 #Hr destruct
+  /3 width=1 by in_comp_unwind2_path_term, in_comp_abst_hd/
+]
+qed.
+
+lemma unwind2_term_appl (f) (v) (t):
+      ＠▼[f]v.▼[f]t ⇔ ▼[f]＠v.t.
+#f #v #t @conj #p #Hp
+[ elim (in_comp_inv_appl … Hp) -Hp * #q #H1 * #r #Hr #H2 destruct
+  /3 width=1 by in_comp_unwind2_path_term, in_comp_appl_sd, in_comp_appl_hd/
+| elim Hp -Hp #q #Hq #H0 destruct
+  elim (in_comp_inv_appl … Hq) -Hq * #r #H0 #Hr destruct
+  /3 width=1 by in_comp_unwind2_path_term, in_comp_appl_sd, in_comp_appl_hd/
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_eq.ma
new file mode 100644
index 000000000..46e539e4e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_eq.ma
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(**) (* reverse include *)
+include "ground/lib/subset_ext_equivalence.ma".
+include "delayed_updating/unwind_k/unwind2_path_eq.ma".
+include "delayed_updating/unwind_k/unwind2_prototerm.ma".
+
+(* TAILED UNWIND FOR PROTOTERM **********************************************)
+
+(* Constructions with subset_equivalence ************************************)
+
+lemma unwind2_term_eq_repl_sn (f1) (f2) (t):
+      f1 ≗ f2 → ▼[f1]t ⇔ ▼[f2]t.
+/3 width=1 by subset_equivalence_ext_f1_exteq, unwind2_path_eq_repl/
+qed.
+
+lemma unwind2_term_eq_repl_dx (f) (t1) (t2):
+      t1 ⇔ t2 → ▼[f]t1 ⇔ ▼[f]t2.
+/2 width=1 by subset_equivalence_ext_f1_bi/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_inner.ma
new file mode 100644
index 000000000..1831a18f2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_inner.ma
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/unwind2_prototerm.ma".
+include "delayed_updating/unwind_k/unwind2_path_append.ma".
+include "ground/lib/subset_overlap.ma".
+
+(* TAILED UNWIND FOR PROTOTERM **********************************************)
+
+(* Destructions with pic ****************************************************)
+
+lemma unwind2_term_des_pic (f) (t):
+      ▼[f]t ≬ 𝐈 → t ≬ 𝐈.
+#f #t * #p * #q #Hq #H0 #Hp destruct
+@(subset_ol_i … Hq) -Hq (**) (* auto does not work *)
+@(unwind2_path_des_pic … Hp)
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_lift.ma
new file mode 100644
index 000000000..e37e7f71b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_prototerm_lift.ma
@@ -0,0 +1,39 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(**) (* reverse include *)
+include "ground/lib/subset_ext_equivalence.ma".
+include "delayed_updating/substitution/lift_prototerm.ma".
+include "delayed_updating/unwind_k/unwind2_path_lift.ma".
+include "delayed_updating/unwind_k/unwind2_prototerm.ma".
+
+(* TAILED UNWIND FOR PROTOTERM **********************************************)
+
+(* Constructions with lift_prototerm ****************************************)
+
+lemma lift_unwind2_term_after (f1) (f2) (t):
+      🠡[f2]▼[f1]t ⇔ ▼[f2∘f1]t.
+#f1 #f2 #t @subset_eq_trans
+[| @subset_inclusion_ext_f1_compose ]
+@subset_equivalence_ext_f1_exteq #p
+@lift_unwind2_path_after
+qed.
+
+lemma unwind2_lift_term_after (f1) (f2) (t):
+      ▼[f2]🠡[f1]t ⇔ ▼[f2∘f1]t.
+#f1 #f2 #t @subset_eq_trans
+[| @subset_inclusion_ext_f1_compose ]
+@subset_equivalence_ext_f1_exteq #p
+@unwind2_lift_path_after
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap.ma
new file mode 100644
index 000000000..22a9c6f18
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap.ma
@@ -0,0 +1,92 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/preunwind2_rmap.ma".
+include "delayed_updating/syntax/path.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+rec definition unwind2_rmap (f) (p) on p: tr_map ≝
+match p with
+[ list_empty     ⇒ f
+| list_lcons l q ⇒ ▶[unwind2_rmap f q]l
+].
+
+interpretation
+  "tailed unwind (relocation map)"
+  'BlackRightTriangle f p = (unwind2_rmap f p).
+
+(* Basic constructions ******************************************************)
+
+lemma unwind2_rmap_empty (f):
+      f = ▶[f]𝐞.
+// qed.
+
+lemma unwind2_rmap_rcons (f) (p) (l):
+      ▶[▶[f]p]l = ▶[f](p◖l).
+// qed.
+
+lemma unwind2_rmap_d_dx (f) (p) (k:pnat):
+      ▶[f]p∘𝐮❨k❩ = ▶[f](p◖𝗱k).
+// qed.
+
+lemma unwind2_rmap_m_dx (f) (p):
+      ▶[f]p = ▶[f](p◖𝗺).
+// qed.
+
+lemma unwind2_rmap_L_dx (f) (p):
+      (⫯▶[f]p) = ▶[f](p◖𝗟).
+// qed.
+
+lemma unwind2_rmap_A_dx (f) (p):
+      ▶[f]p = ▶[f](p◖𝗔).
+// qed.
+
+lemma unwind2_rmap_S_dx (f) (p):
+      ▶[f]p = ▶[f](p◖𝗦).
+// qed.
+
+(* Constructions with path_append *******************************************)
+
+lemma unwind2_rmap_append (f) (p) (q):
+      ▶[▶[f]p]q = ▶[f](p●q).
+#f #p #q elim q -q // #l #q #IH
+<unwind2_rmap_rcons <unwind2_rmap_rcons //
+qed.
+
+(* Constructions with path_lcons ********************************************)
+
+lemma unwind2_rmap_lcons (f) (p) (l):
+      ▶[▶[f]l]p = ▶[f](l◗p).
+// qed.
+
+lemma unwind2_rmap_d_sn (f) (p) (k:pnat):
+      ▶[f∘𝐮❨k❩]p = ▶[f](𝗱k◗p).
+// qed.
+
+lemma unwind2_rmap_m_sn (f) (p):
+      ▶[f]p = ▶[f](𝗺◗p).
+// qed.
+
+lemma unwind2_rmap_L_sn (f) (p):
+      ▶[⫯f]p = ▶[f](𝗟◗p).
+// qed.
+
+lemma unwind2_rmap_A_sn (f) (p):
+      ▶[f]p = ▶[f](𝗔◗p).
+// qed.
+
+lemma unwind2_rmap_S_sn (f) (p):
+      ▶[f]p = ▶[f](𝗦◗p).
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_after.ma
new file mode 100644
index 000000000..b33afdf76
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_after.ma
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/unwind2_rmap.ma".
+include "delayed_updating/syntax/path_structure.ma".
+include "ground/relocation/tr_compose_compose.ma".
+include "ground/relocation/tr_compose_pn.ma".
+include "ground/relocation/tr_compose_eq.ma".
+include "ground/relocation/tr_pn_eq.ma".
+include "ground/lib/stream_eq_eq.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Constructions with tr_after **********************************************)
+
+lemma unwind2_rmap_after (g) (f) (p:path):
+      ▶[g]⊗p∘▶[f]p ≗ ▶[g∘f]p.
+#g #f #p elim p -p // * [ #k ] #p #IH //
+[ <structure_d_dx <unwind2_rmap_d_dx <unwind2_rmap_d_dx
+  @(stream_eq_canc_sn … (tr_compose_assoc …))
+  /2 width=1 by tr_compose_eq_repl/
+| <structure_L_dx <unwind2_rmap_L_dx <unwind2_rmap_L_dx <unwind2_rmap_L_dx
+  /2 width=1 by tr_push_eq_repl/
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_closed.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_closed.ma
new file mode 100644
index 000000000..3d357e0c7
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_closed.ma
@@ -0,0 +1,101 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/unwind2_rmap_lift.ma".
+include "delayed_updating/unwind_k/unwind2_rmap_eq.ma".
+include "delayed_updating/substitution/lift_rmap_structure.ma".
+include "delayed_updating/syntax/path_closed.ma".
+include "delayed_updating/syntax/path_depth.ma".
+include "ground/relocation/nap.ma".
+include "ground/relocation/tr_pushs_tls.ma".
+include "ground/lib/stream_tls_plus.ma".
+include "ground/lib/stream_eq_eq.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Destructions with cpp ****************************************************)
+
+lemma nap_plus_unwind2_rmap_closed (o) (e) (f) (q) (m) (n):
+      q ϵ 𝐂❨o,n,e❩ →
+      f＠§❨m+e❩+♭q = ▶[f]q＠§❨m+n❩.
+#o #e #f #q #m #n #Hq elim Hq -q -n //
+#q #n [ #k #_ ] #_ #IH
+[ <depth_d_dx <unwind2_rmap_d_dx
+  <tr_compose_nap <tr_uni_nap //
+| <depth_L_dx <unwind2_rmap_L_dx
+  <tr_nap_push <nplus_succ_dx //
+]
+qed-.
+
+lemma nap_unwind2_rmap_closed (o) (f) (q) (n):
+      q ϵ 𝐂❨o,n,𝟎❩ →
+      f＠§❨𝟎❩+♭q = ▶[f]q＠§❨n❩.
+#o #f #q #n #Hn
+/2 width=2 by nap_plus_unwind2_rmap_closed/
+qed-.
+
+lemma nap_plus_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (m) (n):
+      q ϵ 𝐂❨o,n,𝟎❩ →
+      (⫯▶[f]p)＠§❨m❩+♭q = ▶[f](p●𝗟◗q)＠§❨m+n❩.
+#o #f #p #q #m #n #Hn
+/2 width=2 by nap_plus_unwind2_rmap_closed/
+qed-.
+
+lemma nap_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
+      q ϵ 𝐂❨o,n,𝟎❩ →
+      ♭q = ▶[f](p●𝗟◗q)＠§❨n❩.
+#o #f #p #q #n #Hn
+>(nplus_zero_sn n)
+<(nap_plus_unwind2_rmap_append_closed_Lq_dx … Hn) -Hn
+<nplus_zero_sn //
+qed-.
+
+lemma tls_succ_plus_unwind2_rmap_push_closed (o) (f) (q) (n):
+      q ϵ 𝐂❨o,n,𝟎❩ →
+      ∀m. ⇂*[m]f ≗ ⇂*[↑(m+n)]▶[⫯f]q.
+#o #f #q #n #Hn elim Hn -q -n //
+#q #n #k #_ #_ #IH #m
+@(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
+>nrplus_inj_dx >nrplus_inj_sn >nsucc_unfold //
+qed-.
+
+lemma tls_succ_unwind2_rmap_push_closed (o) (f) (q) (n):
+      q ϵ 𝐂❨o,n,𝟎❩ →
+      f ≗ ⇂*[↑n]▶[⫯f]q.
+#o #f #q #n #Hn
+/2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
+qed-.
+
+lemma tls_succ_plus_unwind2_rmap_append_closed_Lq_dx (o) (f) (p) (q) (n):
+      q ϵ 𝐂❨o,n,𝟎❩ →
+      ∀m. ⇂*[m]▶[f]p ≗ ⇂*[↑(m+n)]▶[f](p●𝗟◗q).
+#o #f #p #q #n #Hn #m
+/2 width=2 by tls_succ_plus_unwind2_rmap_push_closed/
+qed-.
+
+lemma tls_succ_unwind2_rmap_closed (f) (q) (n):
+      q ϵ 𝐂❨Ⓕ,n,𝟎❩ →
+      ⇂f ≗ ⇂*[↑n]▶[f]q.
+#f #q #n #Hn
+@(stream_eq_canc_dx … (stream_tls_eq_repl …))
+[| @(unwind2_rmap_eq_repl … (tr_compose_id_dx …)) | skip ]
+@(stream_eq_trans … (stream_tls_eq_repl …))
+[| @(lift_unwind2_rmap_after … ) | skip ]
+<tr_compose_tls <tr_id_unfold
+@(stream_eq_trans … (tr_compose_eq_repl …))
+[| @(tls_succ_unwind2_rmap_push_closed … Hn) | skip | // | skip ]
+@(stream_eq_trans ????? (tr_compose_id_dx …))
+<tr_pap_succ_nap <(nap_unwind2_rmap_closed … Hn) <nplus_zero_sn
+<lift_rmap_structure <stream_tls_succ <tr_tls_pushs //
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_crux.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_crux.ma
new file mode 100644
index 000000000..2f5b3c8b6
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_crux.ma
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/unwind2_rmap_closed.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Crucial constructions with tr_uni ****************************************)
+
+(* Note: crux of the commutation between unwind and balanced focused reduction *)
+lemma unwind2_rmap_uni_crux (f) (p) (b) (q) (m) (n):
+      b ϵ 𝐂❨Ⓕ,m,𝟎❩ → q ϵ 𝐂❨Ⓕ,n,𝟎❩ →
+      (𝐮❨↑(♭b+♭q)❩ ∘ ▶[f]p ≗ ▶[f](p●𝗔◗b●𝗟◗q) ∘ 𝐮❨↑(m+n)❩).
+#f #p #b #q #m #n #Hm #Hn
+<list_append_rcons_sn <list_append_rcons_sn >list_append_assoc
+>list_append_rcons_sn >(list_append_rcons_sn … b)
+@(stream_eq_trans … (tr_compose_uni_dx_pap …)) <tr_pap_succ_nap
+@(stream_eq_trans ????? (tr_compose_eq_repl …))
+[| @tls_succ_plus_unwind2_rmap_append_closed_Lq_dx // | skip
+|  <nap_plus_unwind2_rmap_append_closed_Lq_dx // | skip
+] -Hn
+@tr_eq_inv_nap_zero_tl_bi
+[ <tr_compose_nap <tr_compose_nap <tr_uni_nap <tr_uni_nap
+  >nsucc_unfold >nplus_succ_dx >nplus_succ_dx <nplus_assoc <nplus_assoc
+  >tr_nap_plus_dx <unwind2_rmap_append <nap_plus_unwind2_rmap_closed
+  /2 width=4 by pcc_A_sn/
+| @(stream_eq_canc_sn … (tr_tl_compose_uni_sn …))
+  @(stream_eq_trans ????? (tr_tl_compose_uni_sn …))
+  >stream_tls_succ <unwind2_rmap_append
+  /3 width=2 by tls_succ_unwind2_rmap_closed, pcc_A_sn/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_depth.ma
new file mode 100644
index 000000000..6aa48f280
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_depth.ma
@@ -0,0 +1,58 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/unwind2_path_append.ma".
+include "delayed_updating/syntax/path_depth.ma".
+include "ground/relocation/tr_id_compose.ma".
+include "ground/relocation/tr_compose_compose.ma".
+include "ground/relocation/tr_compose_eq.ma".
+include "ground/relocation/xap.ma".
+include "ground/lib/stream_eq_eq.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Constructions with depth *************************************************)
+
+lemma unwind2_rmap_decompose (p) (f):
+      ▶[f]p ≗ (⫯*[♭p]f)∘(▶[𝐢]p).
+#p elim p -p
+[ #f <unwind2_rmap_empty <unwind2_rmap_empty <tr_pushs_zero //
+| * [ #k ] #p #IH #f //
+  [ <unwind2_rmap_d_dx <unwind2_rmap_d_dx <depth_d_dx
+    @(stream_eq_trans … (tr_compose_assoc …))
+    /2 width=1 by tr_compose_eq_repl/
+  | <unwind2_rmap_L_dx <unwind2_rmap_L_dx <depth_L_dx
+    <tr_pushs_succ <tr_compose_push_bi
+    /2 width=1 by tr_push_eq_repl/
+  ]
+]
+qed.
+
+lemma unwind2_rmap_pap_le (f) (p) (h):
+      ▶[𝐢]p＠⧣❨h❩ < ↑♭p → ▶[𝐢]p＠⧣❨h❩ = ▶[f]p＠⧣❨h❩.
+#f #p #h #Hh
+>(tr_pap_eq_repl … (▶[f]p) … (unwind2_rmap_decompose …))
+<tr_compose_pap <tr_pap_pushs_le //
+qed.
+
+lemma unwind2_rmap_xap_le (f) (p) (n):
+      ▶[𝐢]p＠❨n❩ ≤ ♭p → ▶[𝐢]p＠❨n❩ = ▶[f]p＠❨n❩.
+(*
+#f #p * // #h <tr_xap_ninj #Hh
+>unwind2_rmap_pap_le
+*)
+#f #p #n #Hn
+>(tr_xap_eq_repl … (▶[f]p) … (unwind2_rmap_decompose …))
+<tr_compose_xap <tr_xap_pushs_le //
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_eq.ma
new file mode 100644
index 000000000..374a2312a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_eq.ma
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/unwind2_rmap.ma".
+include "delayed_updating/unwind_k/preunwind2_rmap_eq.ma".
+include "ground/relocation/tr_uni_compose.ma".
+include "ground/arith/nat_rplus_pplus.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Constructions with tr_map_eq *********************************************)
+
+lemma unwind2_rmap_eq_repl (p):
+      stream_eq_repl … (λf1,f2. ▶[f1]p ≗ ▶[f2]p).
+#p elim p -p //
+#l #p #IH #f1 #f2 #Hf
+/3 width=1 by preunwind2_rmap_eq_repl/
+qed-.
+
+lemma tls_unwind2_rmap_d_dx (f) (p) (h) (k):
+      ⇂*[h+k]▶[f]p ≗ ⇂*[h]▶[f](p◖𝗱k).
+#f #p #h #k
+<unwind2_rmap_d_dx >nrplus_inj_dx
+/2 width=1 by tr_tls_compose_uni_dx/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_lift.ma
new file mode 100644
index 000000000..1d3d54458
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_lift.ma
@@ -0,0 +1,43 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/unwind2_rmap.ma".
+include "delayed_updating/unwind_k/preunwind2_rmap_lift.ma".
+include "delayed_updating/unwind_k/preunwind2_rmap_eq.ma".
+include "delayed_updating/substitution/lift_path.ma".
+include "delayed_updating/syntax/path_structure.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Constructions with lift_path *********************************************)
+
+lemma lift_unwind2_rmap_after (g) (f) (p):
+      🠢[g]⊗p∘▶[f]p ≗ ▶[g∘f]p.
+#g #f #p elim p -p //
+* [ #k ] #p #IH //
+[ <unwind2_rmap_d_dx <unwind2_rmap_d_dx
+  @(stream_eq_canc_sn … (tr_compose_assoc …))
+  /2 width=1 by tr_compose_eq_repl/
+| <unwind2_rmap_L_dx <unwind2_rmap_L_dx <lift_rmap_L_dx
+  /2 width=1 by tr_push_eq_repl/
+]
+qed.
+
+lemma unwind2_lift_rmap_after (g) (f) (p:path):
+      ▶[g]🠡[f]p∘🠢[f]p ≗ ▶[g∘f]p.
+#g #f #p elim p -p // #l #p #IH
+<lift_path_rcons <lift_rmap_rcons <unwind2_rmap_rcons <unwind2_rmap_rcons
+@(stream_eq_trans … (preunwind2_lift_rmap_after …))
+/2 width=1 by preunwind2_rmap_eq_repl/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_structure.ma
new file mode 100644
index 000000000..c11158af5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind_k/unwind2_rmap_structure.ma
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "delayed_updating/unwind_k/unwind2_rmap.ma".
+include "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/syntax/path_depth.ma".
+include "ground/relocation/tr_pushs.ma".
+
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
+
+(* Constructions with structure and depth ***********************************)
+
+lemma unwind2_rmap_structure (f) (p):
+      (⫯*[♭p]f) = ▶[f]⊗p.
+#f #p elim p -p //
+* [ #k ] #p #IH //
+[ <unwind2_rmap_L_dx //
+| <unwind2_rmap_A_dx //
+| <unwind2_rmap_S_dx //
+]
+qed.