From 61bc42e04598a9f5e489c3867af72e700c7fda04 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 7 Aug 2022 00:20:11 +0200
Subject: [PATCH] partial commit in delayed_updating

+ reversing paths in component "unwind"
---
 .../black_diamond_2.etc}                      |   0
 .../black_downtriangle_1.etc}                 |   0
 .../black_righttriangle_1.etc}                |   0
 .../delayed_updating/etc/unwind2_rmap.etc     |   5 +
 .../substitution/lift_path.ma                 |   1 -
 .../substitution/lift_rmap_eq.ma              |  12 +-
 .../delayed_updating/syntax/path_inner.ma     |  34 +++
 .../delayed_updating/syntax/path_structure.ma | 157 ++++++++++
 .../unwind/preunwind2_rmap.ma                 |  55 ++++
 ...ind_gen_after.ma => preunwind2_rmap_eq.ma} |  18 +-
 .../unwind/preunwind2_rmap_lift.ma            |  34 +++
 .../unwind/unwind2_constructors.ma            |  21 +-
 .../delayed_updating/unwind/unwind2_path.ma   | 180 +++++++++---
 .../unwind2_path_after.ma}                    |  21 +-
 .../unwind/unwind2_path_append.ma             | 244 ++++++++++++++++
 .../unwind/unwind2_path_eq.ma                 |  22 +-
 .../unwind/unwind2_path_lift.ma               |  44 ++-
 .../unwind/unwind2_path_structure.ma          | 123 --------
 .../unwind/unwind2_preterm_eq.ma              |  26 +-
 .../unwind/unwind2_preterm_fsubst.ma          |  20 +-
 .../unwind/unwind2_prototerm.ma               |   2 +-
 ...d_gen_eq.ma => unwind2_prototerm_after.ma} |  27 +-
 .../unwind/unwind2_prototerm_eq.ma            |  11 +-
 .../unwind/unwind2_prototerm_inner.ma         |   4 +-
 .../unwind/unwind2_prototerm_lift.ma          |   6 +-
 .../delayed_updating/unwind/unwind2_rmap.ma   |  89 +++---
 .../unwind/unwind2_rmap_after.ma              |  36 +++
 .../unwind/unwind2_rmap_eq.ma                 |  24 +-
 .../unwind/unwind2_rmap_head.ma               | 107 +++----
 .../unwind/unwind2_rmap_labels.ma             |   4 +-
 .../unwind/unwind2_rmap_lift.ma               |  43 +++
 .../unwind/unwind2_rmap_structure.ma          |  13 +-
 .../delayed_updating/unwind/unwind_gen.ma     |  86 ------
 .../unwind/unwind_gen_structure.ma            | 269 ------------------
 34 files changed, 954 insertions(+), 784 deletions(-)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{notation/functions/black_diamond_2.ma => etc/black_diamond_2.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{notation/functions/black_downtriangle_1.ma => etc/black_downtriangle_1.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{notation/functions/black_righttriangle_1.ma => etc/black_righttriangle_1.etc} (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap.etc
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap.ma
 rename matita/matita/contribs/lambdadelta/delayed_updating/unwind/{unwind_gen_after.ma => preunwind2_rmap_eq.ma} (70%)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_lift.ma
 rename matita/matita/contribs/lambdadelta/delayed_updating/{notation/functions/uparrow_4.ma => unwind/unwind2_path_after.ma} (66%)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_structure.ma
 rename matita/matita/contribs/lambdadelta/delayed_updating/unwind/{unwind_gen_eq.ma => unwind2_prototerm_after.ma} (61%)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_after.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_lift.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_diamond_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/black_diamond_2.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_diamond_2.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/black_diamond_2.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/black_downtriangle_1.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_1.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/black_downtriangle_1.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_righttriangle_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/black_righttriangle_1.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_righttriangle_1.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/black_righttriangle_1.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap.etc
new file mode 100644
index 000000000..7a18aa34e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2_rmap.etc
@@ -0,0 +1,5 @@
+include "delayed_updating/notation/functions/black_righttriangle_1.ma".
+
+interpretation
+  "unwind map (reversed path)"
+  'BlackRightTriangle p = (unwind2_rmap tr_id p).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path.ma
index 1ffe94862..2154e4a55 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path.ma
@@ -14,7 +14,6 @@
 
 include "delayed_updating/substitution/prelift_label.ma".
 include "delayed_updating/substitution/lift_rmap.ma".
-include "ground/xoa/ex_3_2.ma".
 
 (* LIFT FOR PATH ************************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_eq.ma
index a2f841e43..bf5151f00 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_eq.ma
@@ -13,9 +13,8 @@
 (**************************************************************************)
 
 include "delayed_updating/substitution/lift_rmap.ma".
-include "ground/relocation/tr_pn_eq.ma".
+include "delayed_updating/substitution/prelift_rmap_eq.ma".
 include "ground/lib/stream_tls_plus.ma".
-include "ground/lib/stream_tls_eq.ma".
 include "ground/arith/nat_plus_rplus.ma".
 include "ground/arith/nat_rplus_pplus.ma".
 
@@ -26,13 +25,8 @@ include "ground/arith/nat_rplus_pplus.ma".
 lemma lift_rmap_eq_repl (p):
       stream_eq_repl … (λf1,f2. ↑[p]f1 ≗ ↑[p]f2).
 #p elim p -p //
-* [ #k ] #p #IH #f1 #f2 #Hf
-[ /3 width=1 by stream_tls_eq_repl/
-| /2 width=1 by/
-| /3 width=1 by tr_push_eq_repl/
-| /2 width=1 by/
-| /2 width=1 by/
-]
+#l #p #IH #f1 #f2 #Hf
+/3 width=1 by prelift_rmap_eq_repl/
 qed.
 
 lemma tls_lift_rmap_d_dx (f) (p) (n) (k):
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
index 98501e8df..0db6d2f65 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_inner.ma
@@ -59,3 +59,37 @@ lemma pic_inv_d_dx (p) (k):
       p◖𝗱k ϵ 𝐈 → ⊥.
 #p #k #H0 @H0 -H0 //
 qed-.
+
+(* Constructions with path_lcons ********************************************)
+
+lemma pic_m_sn (p):
+      p ϵ 𝐈 → 𝗺◗p ϵ 𝐈.
+* [| * [ #k ] #p #Hp <list_cons_shift ] //
+[ #_ <list_cons_comm //
+| elim (pic_inv_d_dx … Hp)
+]
+qed.
+
+lemma pic_L_sn (p):
+      p ϵ 𝐈 → 𝗟◗p ϵ 𝐈.
+* [| * [ #k ] #p #Hp <list_cons_shift ] //
+[ #_ <list_cons_comm //
+| elim (pic_inv_d_dx … Hp)
+]
+qed.
+
+lemma pic_A_sn (p):
+      p ϵ 𝐈 → 𝗔◗p ϵ 𝐈.
+* [| * [ #k ] #p #Hp <list_cons_shift ] //
+[ #_ <list_cons_comm //
+| elim (pic_inv_d_dx … Hp)
+]
+qed.
+
+lemma pic_S_sn (p):
+      p ϵ 𝐈 → 𝗦◗p ϵ 𝐈.
+* [| * [ #k ] #p #Hp <list_cons_shift ] //
+[ #_ <list_cons_comm //
+| elim (pic_inv_d_dx … Hp)
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
index a9d9dd18f..3b91954fd 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_structure.ma
@@ -14,6 +14,7 @@
 
 include "delayed_updating/syntax/path.ma".
 include "delayed_updating/notation/functions/circled_times_1.ma".
+include "ground/xoa/ex_3_2.ma".
 
 (* STRUCTURE FOR PATH *******************************************************)
 
@@ -99,3 +100,159 @@ lemma structure_S_sn (p):
       (𝗦◗⊗p) = ⊗(𝗦◗p).
 #p <structure_append //
 qed.
+
+(* Basic inversions *********************************************************)
+
+lemma eq_inv_d_dx_structure (h) (q) (p):
+      q◖𝗱h = ⊗p → ⊥.
+#h #q #p elim p -p [| * [ #k ] #p #IH ]
+[ <structure_empty #H0 destruct
+| <structure_d_dx #H0 /2 width=1 by/
+| <structure_m_dx #H0 /2 width=1 by/
+| <structure_L_dx #H0 destruct
+| <structure_A_dx #H0 destruct
+| <structure_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_m_dx_structure (q) (p):
+      q◖𝗺 = ⊗p → ⊥.
+#q #p elim p -p [| * [ #k ] #p #IH ]
+[ <structure_empty #H0 destruct
+| <structure_d_dx #H0 /2 width=1 by/
+| <structure_m_dx #H0 /2 width=1 by/
+| <structure_L_dx #H0 destruct
+| <structure_A_dx #H0 destruct
+| <structure_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_L_dx_structure (q) (p):
+      q◖𝗟 = ⊗p →
+      ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗟◗r2 = p.
+#q #p elim p -p [| * [ #k ] #p #IH ]
+[ <structure_empty #H0 destruct
+| <structure_d_dx #H0
+  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
+  /2 width=5 by ex3_2_intro/
+| <structure_m_dx #H0
+  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
+  /2 width=5 by ex3_2_intro/
+| <structure_L_dx #H0 destruct -IH
+  /2 width=5 by ex3_2_intro/
+| <structure_A_dx #H0 destruct
+| <structure_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_A_dx_structure (q) (p):
+      q◖𝗔 = ⊗p →
+      ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗔◗r2 = p.
+#q #p elim p -p [| * [ #k ] #p #IH ]
+[ <structure_empty #H0 destruct
+| <structure_d_dx #H0
+  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
+  /2 width=5 by ex3_2_intro/
+| <structure_m_dx #H0
+  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
+  /2 width=5 by ex3_2_intro/
+| <structure_L_dx #H0 destruct
+| <structure_A_dx #H0 destruct -IH
+  /2 width=5 by ex3_2_intro/
+| <structure_S_dx #H0 destruct
+]
+qed-.
+
+lemma eq_inv_S_dx_structure (q) (p):
+      q◖𝗦 = ⊗p →
+      ∃∃r1,r2. q = ⊗r1 & 𝐞 = ⊗r2 & r1●𝗦◗r2 = p.
+#q #p elim p -p [| * [ #k ] #p #IH ]
+[ <structure_empty #H0 destruct
+| <structure_d_dx #H0
+  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
+  /2 width=5 by ex3_2_intro/
+| <structure_m_dx #H0
+  elim IH -IH // -H0 #r1 #r2 #H1 #H0 #H2 destruct
+  /2 width=5 by ex3_2_intro/
+| <structure_L_dx #H0 destruct
+| <structure_A_dx #H0 destruct
+| <structure_S_dx #H0 destruct -IH
+  /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+(* Main inversions **********************************************************)
+
+theorem eq_inv_append_structure (p) (q) (r):
+        p●q = ⊗r →
+        ∃∃r1,r2.p = ⊗r1 & q = ⊗r2 & r1●r2 = r.
+#p #q elim q -q [| * [ #k ] #q #IH ] #r
+[ <list_append_empty_sn #H0 destruct
+  /2 width=5 by ex3_2_intro/
+| #H0 elim (eq_inv_d_dx_structure … H0)
+| #H0 elim (eq_inv_m_dx_structure … H0)
+| #H0 elim (eq_inv_L_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
+  elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
+  @(ex3_2_intro … s1 (s2●𝗟◗r2)) //
+  <structure_append <structure_L_sn <Hr2 -Hr2 //
+| #H0 elim (eq_inv_A_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
+  elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
+  @(ex3_2_intro … s1 (s2●𝗔◗r2)) //
+  <structure_append <structure_A_sn <Hr2 -Hr2 //
+| #H0 elim (eq_inv_S_dx_structure … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
+  elim (IH … Hr1) -IH -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
+  @(ex3_2_intro … s1 (s2●𝗦◗r2)) //
+  <structure_append <structure_S_sn <Hr2 -Hr2 //
+]
+qed-.
+
+(* Inversions with path_lcons ***********************************************)
+
+lemma eq_inv_d_sn_structure (h) (q) (p):
+      (𝗱h◗q) = ⊗p → ⊥.
+#h #q #p >list_cons_comm #H0
+elim (eq_inv_append_structure … H0) -H0 #r1 #r2
+<list_cons_comm #H0 #H1 #H2 destruct
+elim (eq_inv_d_dx_structure … H0)
+qed-.
+
+lemma eq_inv_m_sn_structure (q) (p):
+      (𝗺 ◗q) = ⊗p → ⊥.
+#q #p >list_cons_comm #H0
+elim (eq_inv_append_structure … H0) -H0 #r1 #r2
+<list_cons_comm #H0 #H1 #H2 destruct
+elim (eq_inv_m_dx_structure … H0)
+qed-.
+
+lemma eq_inv_L_sn_structure (q) (p):
+      (𝗟◗q) = ⊗p →
+      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ⊗r2 & r1●𝗟◗r2 = p.
+#q #p >list_cons_comm #H0
+elim (eq_inv_append_structure … H0) -H0 #r1 #r2
+<list_cons_comm #H0 #H1 #H2 destruct
+elim (eq_inv_L_dx_structure … H0) -H0 #s1 #s2 #H1 #H2 #H3 destruct
+@(ex3_2_intro … s1 (s2●r2)) // -s1
+<structure_append <H2 -s2 //
+qed-.
+
+lemma eq_inv_A_sn_structure (q) (p):
+      (𝗔◗q) = ⊗p →
+      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ⊗r2 & r1●𝗔◗r2 = p.
+#q #p >list_cons_comm #H0
+elim (eq_inv_append_structure … H0) -H0 #r1 #r2
+<list_cons_comm #H0 #H1 #H2 destruct
+elim (eq_inv_A_dx_structure … H0) -H0 #s1 #s2 #H1 #H2 #H3 destruct
+@(ex3_2_intro … s1 (s2●r2)) // -s1
+<structure_append <H2 -s2 //
+qed-.
+
+lemma eq_inv_S_sn_structure (q) (p):
+      (𝗦◗q) = ⊗p →
+      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ⊗r2 & r1●𝗦◗r2 = p.
+#q #p >list_cons_comm #H0
+elim (eq_inv_append_structure … H0) -H0 #r1 #r2
+<list_cons_comm #H0 #H1 #H2 destruct
+elim (eq_inv_S_dx_structure … H0) -H0 #s1 #s2 #H1 #H2 #H3 destruct
+@(ex3_2_intro … s1 (s2●r2)) // -s1
+<structure_append <H2 -s2 //
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap.ma
new file mode 100644
index 000000000..d6cdbce3d
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/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/unwind_gen_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_eq.ma
similarity index 70%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_eq.ma
index 2954be831..32efd9f04 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/preunwind2_rmap_eq.ma
@@ -12,14 +12,16 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/unwind/unwind_gen.ma".
-include "ground/relocation/tr_compose_pap.ma".
+include "delayed_updating/unwind/preunwind2_rmap.ma".
+include "ground/relocation/tr_compose_eq.ma".
+include "ground/relocation/tr_pn_eq.ma".
 
-(* GENERIC UNWIND FOR PATH **************************************************)
+(* TAILED PREUNWIND FOR RELOCATION MAP **************************************)
 
-(* Properties with tr_compose ***********************************************)
+(* Constructions with tr_map_eq *********************************************)
 
-lemma unwind_gen_after (f2) (f1) (p):
-      ◆[f2]◆[f1]p = ◆[f2∘f1]p.
-#f2 #f1 #p @(path_ind_unwind … p) -p //
-qed.
+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
new file mode 100644
index 000000000..f5317dbf3
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/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/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∘↑[l]f ≗ ▶[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_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma
index 8cdfb5bf9..35fa984b5 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma
@@ -13,27 +13,28 @@
 (**************************************************************************)
 
 include "delayed_updating/unwind/unwind2_prototerm_eq.ma".
+include "delayed_updating/unwind/unwind2_path_append.ma".
 include "delayed_updating/syntax/prototerm_constructors.ma".
 
-(* UNWIND FOR PROTOTERM *****************************************************)
+(* TAILED UNWIND FOR PROTOTERM **********************************************)
 
 (* Constructions with constructors ******************************************)
 
-lemma unwind2_term_iref_sn (f) (t) (n:pnat):
-      ▼[f∘𝐮❨n❩]t ⊆ ▼[f](𝛕n.t).
-#f #t #n #p * #q #Hq #H0 destruct
-@(ex2_intro … (𝗱n◗𝗺◗q))
+lemma unwind2_term_iref_sn (f) (t) (k:pnat):
+      ▼[f∘𝐮❨k❩]t ⊆ ▼[f](𝛕k.t).
+#f #t #k #p * #q #Hq #H0 destruct
+@(ex2_intro … (𝗱k◗𝗺◗q))
 /2 width=1 by in_comp_iref/
 qed-.
 
-lemma unwind2_term_iref_dx (f) (t) (n:pnat):
-      ▼[f](𝛕n.t) ⊆ ▼[f∘𝐮❨n❩]t.
-#f #t #n #p * #q #Hq #H0 destruct
+lemma unwind2_term_iref_dx (f) (t) (k:pnat):
+      ▼[f](𝛕k.t) ⊆ ▼[f∘𝐮❨k❩]t.
+#f #t #k #p * #q #Hq #H0 destruct
 elim (in_comp_inv_iref … Hq) -Hq #p #Hp #Ht destruct
 /2 width=1 by in_comp_unwind2_path_term/
 qed-.
 
-lemma unwind2_term_iref (f) (t) (n:pnat):
-      ▼[f∘𝐮❨n❩]t ⇔ ▼[f](𝛕n.t).
+lemma unwind2_term_iref (f) (t) (k:pnat):
+      ▼[f∘𝐮❨k❩]t ⇔ ▼[f](𝛕k.t).
 /3 width=2 by conj, unwind2_term_iref_sn, unwind2_term_iref_dx/
 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
index 3288fc734..08115e1e4 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path.ma
@@ -12,73 +12,159 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/unwind/unwind_gen.ma".
 include "delayed_updating/unwind/unwind2_rmap.ma".
-include "delayed_updating/syntax/path_reverse.ma".
+include "delayed_updating/syntax/path_structure.ma".
 include "delayed_updating/notation/functions/black_downtriangle_2.ma".
-include "ground/lib/list_tl.ma".
 
-(* UNWIND FOR PATH **********************************************************)
+(* TAILED UNWIND FOR PATH ***************************************************)
 
 definition unwind2_path (f) (p): path ≝
-           ◆[▶[f]⇂(pᴿ)]p
-.
+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
-  "unwind (path)"
+  "tailed unwind (path)"
   'BlackDownTriangle f p = (unwind2_path f p).
 
 (* Basic constructions ******************************************************)
 
-lemma unwind2_path_unfold (f) (p):
-      ◆[▶[f]⇂(pᴿ)]p = ▼[f]p.
-// qed.
-
 lemma unwind2_path_empty (f):
       (𝐞) = ▼[f]𝐞.
 // qed.
 
-lemma unwind2_path_d_empty (f) (n):
-      (𝗱(f＠⧣❨n❩)◗𝐞) = ▼[f](𝗱n◗𝐞).
+lemma unwind2_path_d_dx (f) (p) (k) :
+      (⊗p)◖𝗱((▶[f]p)＠⧣❨k❩) = ▼[f](p◖𝗱k).
 // qed.
 
-lemma unwind2_path_d_lcons (f) (p) (l) (n:pnat):
-      ▼[f∘𝐮❨n❩](l◗p) = ▼[f](𝗱n◗l◗p).
-#f #p #l #n <unwind2_path_unfold <unwind2_path_unfold
-<unwind_gen_d_lcons <reverse_lcons
-@(list_ind_rcons … p) -p // #p #l0 #_
-<reverse_rcons <reverse_lcons <reverse_lcons <reverse_rcons
-<list_tl_lcons <list_tl_lcons //
-qed.
+lemma unwind2_path_m_dx (f) (p):
+      ⊗p = ▼[f](p◖𝗺).
+// qed.
 
-lemma unwind2_path_m_sn (f) (p):
-      ▼[f]p = ▼[f](𝗺◗p).
-#f #p <unwind2_path_unfold <unwind2_path_unfold
-<unwind_gen_m_sn <reverse_lcons
-@(list_ind_rcons … p) -p // #p #l #_
-<reverse_rcons <list_tl_lcons <list_tl_lcons //
-qed.
+lemma unwind2_path_L_dx (f) (p):
+      (⊗p)◖𝗟 = ▼[f](p◖𝗟).
+// qed.
 
-lemma unwind2_path_L_sn (f) (p):
-      (𝗟◗▼[⫯f]p) = ▼[f](𝗟◗p).
-#f #p <unwind2_path_unfold <unwind2_path_unfold
-<unwind_gen_L_sn <reverse_lcons
-@(list_ind_rcons … p) -p // #p #l #_
-<reverse_rcons <list_tl_lcons <list_tl_lcons //
-qed.
+lemma unwind2_path_A_dx (f) (p):
+      (⊗p)◖𝗔 = ▼[f](p◖𝗔).
+// qed.
+
+lemma unwind2_path_S_dx (f) (p):
+      (⊗p)◖𝗦 = ▼[f](p◖𝗦).
+// qed.
 
-lemma unwind2_path_A_sn (f) (p):
-      (𝗔◗▼[f]p) = ▼[f](𝗔◗p).
-#f #p <unwind2_path_unfold <unwind2_path_unfold
-<unwind_gen_A_sn <reverse_lcons
-@(list_ind_rcons … p) -p // #p #l #_
-<reverse_rcons <list_tl_lcons <list_tl_lcons //
+(* Constructions with structure *********************************************)
+
+lemma structure_unwind2_path (f) (p):
+      ⊗p = ⊗▼[f]p.
+#f * // * [ #k ] #p //
 qed.
 
-lemma unwind2_path_S_sn (f) (p):
-      (𝗦◗▼[f]p) = ▼[f](𝗦◗p).
-#f #p <unwind2_path_unfold <unwind2_path_unfold
-<unwind_gen_S_sn <reverse_lcons
-@(list_ind_rcons … p) -p // #p #l #_
-<reverse_rcons <list_tl_lcons <list_tl_lcons //
+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/notation/functions/uparrow_4.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_after.ma
similarity index 66%
rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_4.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_after.ma
index 6d638c86a..c7a3bcf0f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/uparrow_4.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_after.ma
@@ -12,16 +12,17 @@
 (*                                                                        *)
 (**************************************************************************)
 
-(* NOTATION FOR DELAYED UPDATING ********************************************)
+include "delayed_updating/unwind/unwind2_path_eq.ma".
+include "delayed_updating/unwind/unwind2_rmap_after.ma".
 
-notation < "hvbox( ↑❨ term 46 k, break term 46 p, break term 46 f ❩ )"
-  non associative with precedence 70
-  for @{ 'UpArrow $S $k $p $f }.
+(* TAILED UNWIND FOR PATH ***************************************************)
 
-notation > "hvbox( ↑❨ term 46 k, break term 46 p, break term 46 f ❩ )"
-  non associative with precedence 70
-  for @{ 'UpArrow ? $k $p $f }.
+(* Properties with tr_after *************************************************)
 
-notation > "hvbox( ↑{ term 46 S }❨ break term 46 k, break term 46 p, break term 46 f ❩ )"
-  non associative with precedence 70
-  for @{ 'UpArrow $S $k $p $f }.
+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
new file mode 100644
index 000000000..3114e9edd
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/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/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 inner condition for path ******************************)
+
+lemma unwind2_path_inner (f) (p):
+      p ϵ 𝐈 → ⊗p = ▼[f]p.
+#f * // * // #k #q #Hq
+elim (pic_inv_d_dx … Hq)
+qed-.
+
+(* Constructions with append and inner condition for path *******************)
+
+lemma unwind2_path_append_inner_sn (f) (p) (q): p ϵ 𝐈 →
+      (⊗p)●(▼[▶[f]p]q) = ▼[f](p●q).
+#f #p * [ #Hp | * [ #k ] #q #_ ] //
+[ <(unwind2_path_inner … 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 proper condition for path ******************)
+
+lemma unwind2_path_append_proper_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_proper_dx in ⊢ (???%); //
+qed.
+
+lemma unwind2_path_m_sn (f) (p):
+      ▼[f]p = ▼[f](𝗺◗p).
+#f #p <unwind2_path_append_inner_sn //
+qed.
+
+lemma unwind2_path_L_sn (f) (p):
+      (𝗟◗▼[⫯f]p) = ▼[f](𝗟◗p).
+#f #p <unwind2_path_append_inner_sn //
+qed.
+
+lemma unwind2_path_A_sn (f) (p):
+      (𝗔◗▼[f]p) = ▼[f](𝗔◗p).
+#f #p <unwind2_path_append_inner_sn //
+qed.
+
+lemma unwind2_path_S_sn (f) (p):
+      (𝗦◗▼[f]p) = ▼[f](𝗦◗p).
+#f #p <unwind2_path_append_inner_sn //
+qed.
+
+(* Destructions with inner condition for path *******************************)
+
+lemma unwind2_path_des_inner (f) (p):
+      ▼[f]p ϵ 𝐈 → p ϵ 𝐈.
+#f * // * [ #k ] #p //
+<unwind2_path_d_dx #H0
+elim (pic_inv_d_dx … H0)
+qed-.
+
+(* Destructions with append and inner condition for path ********************)
+
+lemma unwind2_path_des_append_inner_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_inner … Hq1) -Hq1 #Hp
+  <(unwind2_path_inner … 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_proper_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_proper_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_proper_dx //
+  <unwind2_path_S_sn <Hr2 -Hr2 //
+]
+qed-.
+
+(* Inversions with append and proper condition for path *********************)
+
+lemma unwind2_path_inv_append_proper_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_proper_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_proper_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_proper_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_proper_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_inner_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_inner_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_proper_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_inner_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_proper_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_inner_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_proper_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
index ed75b0d7a..c1b188b60 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_eq.ma
@@ -14,26 +14,16 @@
 
 include "delayed_updating/unwind/unwind2_path.ma".
 include "delayed_updating/unwind/unwind2_rmap_eq.ma".
-include "delayed_updating/unwind/unwind_gen_eq.ma".
-include "ground/relocation/tr_compose_compose.ma".
 
-(* UNWIND FOR PATH **********************************************************)
+(* TAILED UNWIND FOR PATH ***************************************************)
 
-(* Constructions with stream_eq *********************************************)
+(* Constructions with tr_map_eq *********************************************)
 
 lemma unwind2_path_eq_repl (p):
       stream_eq_repl … (λf1,f2. ▼[f1]p = ▼[f2]p).
-/3 width=1 by unwind2_rmap_eq_repl, unwind_gen_eq_repl/
+* // * [ #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-.
 
-(* Properties with tr_compose ***********************************************)
-
-lemma unwind2_path_after (p) (f1) (f2):
-      ▼[f2]▼[f1]p = ▼[f2∘f1]p.
-#p @(path_ind_unwind … p) -p // [ #n #l #p | #p ] #IH #f1 #f2
-[ <unwind2_path_d_lcons <unwind2_path_d_lcons
-  >(unwind2_path_eq_repl … (tr_compose_assoc …)) //
-| <(unwind2_path_L_sn … f1) <unwind2_path_L_sn <unwind2_path_L_sn
-  >tr_compose_push_bi //
-]
-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
index ac2166a46..5af9e1664 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma
@@ -12,35 +12,31 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/unwind/unwind2_path_eq.ma".
-include "delayed_updating/substitution/lift_path_prelift.ma".
+include "delayed_updating/unwind/unwind2_path.ma".
+include "delayed_updating/unwind/unwind2_rmap_lift.ma".
+include "delayed_updating/substitution/lift_path_structure.ma".
 
-(* UNWIND FOR PATH **********************************************************)
+(* TAILED UNWIND FOR PATH ***************************************************)
 
 (* Constructions with lift_path *********************************************)
 
-lemma lift_unwind2_path_after (p) (f1) (f2):
-      ↑[f2]▼[f1]p = ▼[f2∘f1]p.
-#p @(path_ind_unwind … p) -p // [ #n | #p ] #IH #f1 #f2
-[ <unwind2_path_d_empty <unwind2_path_d_empty
-  <lift_path_d_sn <lift_path_empty //
-| <unwind2_path_L_sn <unwind2_path_L_sn <lift_path_L_sn
-  >tr_compose_push_bi //
-]
+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_path_after_lift (p) (f1) (f2):
-      ▼[f2]↑[f1]p = ▼[f2∘f1]p.
-#p @(path_ind_unwind … p) -p // [ #n #l ] #p #IH #f1 #f2
-[ <lift_path_d_sn <unwind2_path_d_lcons
-  <lift_path_lcons_prelift <unwind2_path_d_lcons >lift_path_lcons_prelift
-  >IH -IH
-  >(unwind2_path_eq_repl … (tr_compose_assoc …))
-  >(unwind2_path_eq_repl … (tr_compose_assoc …))
-  <unwind2_path_after <unwind2_path_after in ⊢ (???%);
-  /3 width=1 by unwind2_path_eq_repl, eq_f/
-| <lift_path_m_sn <unwind2_path_m_sn <unwind2_path_m_sn //
-| <lift_path_L_sn <unwind2_path_L_sn <unwind2_path_L_sn 
-  >tr_compose_push_bi //
+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_path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_structure.ma
deleted file mode 100644
index 9436b0c2a..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_structure.ma
+++ /dev/null
@@ -1,123 +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/unwind_gen_structure.ma".
-
-(* UNWIND FOR PATH **********************************************************)
-
-(* Constructions with list_rcons ********************************************)
-
-lemma unwind2_path_d_dx (f) (p) (n) :
-      (⊗p)◖𝗱((▶[f](pᴿ))＠⧣❨n❩) = ▼[f](p◖𝗱n).
-#f #p #n <unwind2_path_unfold
-<unwind_gen_d_dx //
-qed.
-
-lemma unwind2_path_m_dx (f) (p):
-      ⊗p = ▼[f](p◖𝗺).
-#f #p <unwind2_path_unfold //
-qed.
-
-lemma unwind2_path_L_dx (f) (p):
-      (⊗p)◖𝗟 = ▼[f](p◖𝗟).
-#f #p <unwind2_path_unfold //
-qed.
-
-lemma unwind2_path_A_dx (f) (p):
-      (⊗p)◖𝗔 = ▼[f](p◖𝗔).
-#f #p <unwind2_path_unfold //
-qed.
-
-lemma unwind2_path_S_dx (f) (p):
-      (⊗p)◖𝗦 = ▼[f](p◖𝗦).
-#f #p <unwind2_path_unfold //
-qed.
-
-lemma unwind2_path_root (f) (p):
-      ∃∃r. 𝐞 = ⊗r & ⊗p●r = ▼[f]p.
-#f #p
-elim (unwind_gen_root)
-/2 width=3 by ex2_intro/
-qed-.
-
-(* Constructions with proper condition for path *****************************)
-
-lemma unwind2_path_append_proper_dx (f) (p1) (p2): p2 ϵ 𝐏 →
-      (⊗p1)●(▼[▶[f]p1ᴿ]p2) = ▼[f](p1●p2).
-#f #p1 #p2 #Hp2 <unwind2_path_unfold <unwind2_path_unfold
-<unwind_gen_append_proper_dx // -Hp2 <reverse_append
-@(list_ind_rcons … p2) -p2 // #q2 #l2 #_
-<reverse_rcons <list_tl_lcons <list_tl_lcons //
-qed-.
-
-(* Constructions with inner condition for path ******************************)
-
-lemma unwind2_path_append_inner_sn (f) (p1) (p2): p1 ϵ 𝐈 →
-      (⊗p1)●(▼[▶[f]p1ᴿ]p2) = ▼[f](p1●p2).
-#f #p1 #p2 #Hp1 <unwind2_path_unfold <unwind2_path_unfold
-<unwind_gen_append_inner_sn // -Hp1 <reverse_append
-@(list_ind_rcons … p2) -p2 // #q2 #l2 #_
-<reverse_rcons <list_tl_lcons <list_tl_lcons //
-qed-.
-
-(* Inversions with list_lcons ***********************************************)
-
-lemma unwind2_path_inv_S_sn (f) (p) (q):
-      (𝗦◗q) = ▼[f]p →
-      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▶[f]r1ᴿ]r2 & r1●𝗦◗r2 = p.
-#f #p #q #H0
-elim (unwind_gen_inv_S_sn … H0) -H0 #r1 #r2 #Hr1 #H1 #H2 destruct
-<reverse_append <reverse_lcons
-@(list_ind_rcons … r2) -r2 [ /2 width=5 by ex3_2_intro/ ] #r2 #l2 #_
-<reverse_rcons <list_append_lcons_sn <list_append_rcons_sn
-<list_tl_lcons <unwind2_rmap_append <unwind2_rmap_S_sn
-/2 width=5 by ex3_2_intro/
-qed-.
-
-(* Inversions with proper condition for path ********************************)
-
-lemma unwind2_path_inv_append_proper_dx (f) (p) (q1) (q2):
-      q2 ϵ 𝐏 → q1●q2 = ▼[f]p →
-      ∃∃p1,p2. ⊗p1 = q1 & ▼[▶[f]p1ᴿ]p2 = q2 & p1●p2 = p.
-#f #p #q1 #q2 #Hq2 #H0
-elim (unwind_gen_inv_append_proper_dx … Hq2 H0) -Hq2 -H0
-#p1 #p2 #H1 #H2 #H3 destruct <reverse_append
-@(list_ind_rcons … p2) -p2 [ /2 width=5 by ex3_2_intro/ ] #q2 #l2 #_
-<reverse_rcons <list_tl_lcons <unwind2_rmap_append
-@ex3_2_intro [4: |*: // ] <unwind2_path_unfold // (**) (* auto fails *)
-qed-.
-
-(* Inversions with inner condition for path *********************************)
-
-lemma unwind2_path_inv_append_inner_sn (f) (p) (q1) (q2):
-      q1 ϵ 𝐈 → q1●q2 = ▼[f]p →
-      ∃∃p1,p2. ⊗p1 = q1 & ▼[▶[f]p1ᴿ]p2 = q2 & p1●p2 = p.
-#f #p #q1 #q2 #Hq1 #H0
-elim (unwind_gen_inv_append_inner_sn … Hq1 H0) -Hq1 -H0
-#p1 #p2 #H1 #H2 #H3 destruct <reverse_append
-@(list_ind_rcons … p2) -p2 [ /2 width=5 by ex3_2_intro/ ] #q2 #l2 #_
-<reverse_rcons <list_tl_lcons <unwind2_rmap_append
-@ex3_2_intro [4: |*: // ] <unwind2_path_unfold // (**) (* auto fails *)
-qed-.
-
-(* Destructions with inner condition for path *******************************)
-
-lemma unwind2_path_des_inner (f) (p):
-      ▼[f]p ϵ 𝐈 → p ϵ 𝐈.
-#f #p @(list_ind_rcons … p) -p //
-#p * [ #n ] #_ //
-<unwind2_path_d_dx #H0
-elim (pic_inv_d_dx … H0)
-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
index 9ceccc0e2..57a17a894 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_eq.ma
@@ -13,43 +13,43 @@
 (**************************************************************************)
 
 include "delayed_updating/unwind/unwind2_prototerm.ma".
-include "delayed_updating/unwind/unwind2_path_structure.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".
 
-(* UNWIND FOR PRETERM *******************************************************)
+(* 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]p](t⋔p) ⊆ (▼[f]t)⋔(⊗p).
 #f #t #p #Hp #q * #r #Hr #H0 destruct
 @(ex2_intro … Hr) -Hr
 <unwind2_path_append_inner_sn //
 qed-.
 
 lemma unwind2_term_grafted_dx (f) (t) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
-      (▼[f]t)⋔(⊗p) ⊆ ▼[▶[f]pᴿ](t⋔p).
+      (▼[f]t)⋔(⊗p) ⊆ ▼[▶[f]p](t⋔p).
 #f #t #p #H1p #H2p #Ht #q * #r #Hr #H0
-elim (unwind2_path_inv_append_inner_sn … (sym_eq … H0)) -H0 //
+elim (unwind2_path_des_append_inner_sn … (sym_eq … H0)) -H0 //
 #p0 #q0 #Hp0 #Hq0 #H0 destruct
-<(Ht … Hp0) [|*: /2 width=2 by ex_intro/ ] -p
+>(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).
+      ▼[▶[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)◖𝗦) ⊆ ▼[▶[f]p](t⋔(p◖𝗦)).
 #f #t #p #Hp #Ht #q * #r #Hr
-<list_append_rcons_sn #H0
+>list_append_rcons_sn #H0
 elim (unwind2_path_inv_append_proper_dx … (sym_eq … H0)) -H0 //
 #p0 #q0 #Hp0 #Hq0 #H0 destruct
-<(Ht … Hp0) [|*: /2 width=2 by ex_intro/ ] -p
-elim (unwind2_path_inv_S_sn … (sym_eq … Hq0)) -Hq0
+>(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
@@ -57,10 +57,10 @@ lapply (preterm_in_root_append_inv_structure_empty_dx … p0 … Ht Hr1)
 qed-.
 
 lemma unwind2_term_grafted_S (f) (t) (p): p ϵ ▵t → t ϵ 𝐓 →
-      ▼[▶[f]pᴿ](t⋔(p◖𝗦)) ⇔ (▼[f]t)⋔((⊗p)◖𝗦).
+      ▼[▶[f]p](t⋔(p◖𝗦)) ⇔ (▼[f]t)⋔((⊗p)◖𝗦).
 #f #t #p #Hp #Ht
 @conj
-[ >unwind2_rmap_S_sn >reverse_rcons >structure_S_dx
+[ >unwind2_rmap_S_dx >structure_S_dx
   @unwind2_term_grafted_sn // (**) (* auto fails *)
 | /2 width=1 by unwind2_term_grafted_S_dx/
 ]
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
index 452c913e5..19634dccc 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma
@@ -13,33 +13,33 @@
 (**************************************************************************)
 
 include "delayed_updating/unwind/unwind2_prototerm_eq.ma".
-include "delayed_updating/unwind/unwind2_path_structure.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".
 
-(* UNWIND FOR PRETERM *******************************************************)
+(* TAILED UNWIND FOR PRETERM ************************************************)
 
 (* Constructions with fsubst ************************************************)
 
 lemma unwind2_term_fsubst_sn (f) (t) (u) (p): u ϵ 𝐏 →
-      (▼[f]t)[⋔(⊗p)←▼[▶[f]pᴿ]u] ⊆ ▼[f](t[⋔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_proper_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_dx #H2 destruct
+  [ <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_proper_dx /2 width=3 by ppc_lcons/ ]
+    @H0 -H0 [| <unwind2_path_append_proper_dx /2 width=3 by ppc_rcons/ ]
   ]
 ]
 qed-.
 
 lemma unwind2_term_fsubst_dx (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 𝐓 →
-      ▼[f](t[⋔p←u]) ⊆ (▼[f]t)[⋔(⊗p)←▼[▶[f]pᴿ]u].
+      ▼[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
@@ -47,9 +47,9 @@ lemma unwind2_term_fsubst_dx (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 
   /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_dx #Hr @(H0 … (𝐞)) -H0
-    <list_append_empty_dx @H2p -H2p
-    /2 width=2 by unwind_gen_des_structure, prototerm_in_comp_root/
+  [ <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_proper_dx … Hr) -Hr // #s1 #s2 #Hs1 #_ #H1 destruct
     lapply (H2p … Hs1) -H2p -Hs1 /2 width=2 by ex_intro/
@@ -58,5 +58,5 @@ lemma unwind2_term_fsubst_dx (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 
 qed-.
 
 lemma unwind2_term_fsubst (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 𝐓 →
-      (▼[f]t)[⋔(⊗p)←▼[▶[f]pᴿ]u] ⇔ ▼[f](t[⋔p←u]).
+      (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u] ⇔ ▼[f](t[⋔p←u]).
 /4 width=3 by unwind2_term_fsubst_sn, conj, unwind2_term_fsubst_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
index e0515c7f0..e4e480c66 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm.ma
@@ -16,7 +16,7 @@ include "delayed_updating/unwind/unwind2_path.ma".
 include "delayed_updating/syntax/prototerm.ma".
 include "ground/lib/subset_ext.ma".
 
-(* UNWIND FOR PROTOTERM *****************************************************)
+(* TAILED UNWIND FOR PROTOTERM **********************************************)
 
 interpretation
   "unwind (prototerm)"
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_after.ma
similarity index 61%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_after.ma
index 11ddd2d03..9e7dd82f2 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_after.ma
@@ -12,23 +12,18 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/unwind/unwind_gen.ma".
-include "ground/relocation/tr_pap_eq.ma".
+include "delayed_updating/unwind/unwind2_prototerm_eq.ma".
+include "delayed_updating/unwind/unwind2_path_after.ma".
 
-(* GENERIC UNWIND FOR PATH **************************************************)
+(* TAILED UNWIND FOR PROTOTERM **********************************************)
 
-(* Constructions with stream_eq *********************************************)
+(* Constructions with tr_after **********************************************)
 
-lemma unwind_gen_eq_repl (p):
-      stream_eq_repl … (λf1,f2. ◆[f1]p = ◆[f2]p).
-#p @(path_ind_unwind … p) -p // [ #n |*: #p ] #IH #f1 #f2 #Hf
-[ <unwind_gen_d_empty <unwind_gen_d_empty
-  <(tr_pap_eq_repl … Hf) -f2 -IH //
-| <unwind_gen_L_sn <unwind_gen_L_sn
-  <(IH … Hf) -f2 -IH //
-| <unwind_gen_A_sn <unwind_gen_A_sn
-  <(IH … Hf) -f2 -IH //
-| <unwind_gen_S_sn <unwind_gen_S_sn
-  <(IH … Hf) -f2 -IH //
+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-.
+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
index dbde59810..24e3c7086 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_eq.ma
@@ -17,7 +17,7 @@ include "ground/lib/subset_ext_equivalence.ma".
 include "delayed_updating/unwind/unwind2_path_eq.ma".
 include "delayed_updating/unwind/unwind2_prototerm.ma".
 
-(* UNWIND FOR PROTOTERM *****************************************************)
+(* TAILED UNWIND FOR PROTOTERM **********************************************)
 
 (* Constructions with subset_equivalence ************************************)
 
@@ -30,12 +30,3 @@ 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.
-
-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_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma
index 828f9905b..cbb32a8b5 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma
@@ -13,10 +13,10 @@
 (**************************************************************************)
 
 include "delayed_updating/unwind/unwind2_prototerm.ma".
-include "delayed_updating/unwind/unwind2_path_structure.ma".
+include "delayed_updating/unwind/unwind2_path_append.ma".
 include "ground/lib/subset_overlap.ma".
 
-(* UNWIND FOR PROTOTERM *****************************************************)
+(* TAILED UNWIND FOR PROTOTERM **********************************************)
 
 (* Destructions with inner condition for path *******************************)
 
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
index 8d987dfb7..5b18cfb17 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma
@@ -18,7 +18,7 @@ include "delayed_updating/substitution/lift_prototerm.ma".
 include "delayed_updating/unwind/unwind2_path_lift.ma".
 include "delayed_updating/unwind/unwind2_prototerm.ma".
 
-(* UNWIND FOR PROTOTERM *****************************************************)
+(* TAILED UNWIND FOR PROTOTERM **********************************************)
 
 (* Constructions with lift_prototerm ****************************************)
 
@@ -30,10 +30,10 @@ lemma lift_unwind2_term_after (f1) (f2) (t):
 @lift_unwind2_path_after
 qed.
 
-lemma unwind2_term_after_lift (f1) (f2) (t):
+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_path_after_lift
+@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
index 879af2518..5177fd7ee 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap.ma
@@ -12,92 +12,81 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "delayed_updating/unwind/preunwind2_rmap.ma".
 include "delayed_updating/syntax/path.ma".
-include "delayed_updating/notation/functions/black_righttriangle_2.ma".
-include "delayed_updating/notation/functions/black_righttriangle_1.ma".
-include "ground/relocation/tr_uni.ma".
-include "ground/relocation/tr_compose.ma".
 
-(* UNWIND MAP FOR PATH ******************************************************)
+(* 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 ⇒
-  match l with
-  [ label_d n ⇒ (unwind2_rmap f q)∘𝐮❨n❩
-  | label_m   ⇒ unwind2_rmap f q
-  | label_L   ⇒ ⫯(unwind2_rmap f q)
-  | label_A   ⇒ unwind2_rmap f q
-  | label_S   ⇒ unwind2_rmap f q
-  ]
+| list_lcons l q ⇒ ▶[unwind2_rmap f q]l
 ].
 
 interpretation
-  "tailed unwind map (reversed path)"
+  "tailed unwind (relocation map)"
   'BlackRightTriangle f p = (unwind2_rmap f p).
 
-interpretation
-  "unwind map (reversed path)"
-  'BlackRightTriangle p = (unwind2_rmap tr_id p).
-
 (* Basic constructions ******************************************************)
 
 lemma unwind2_rmap_empty (f):
       f = ▶[f]𝐞.
 // qed.
 
-lemma unwind2_rmap_d_sn (f) (p) (n:pnat):
-      (▶[f]p∘𝐮❨n❩) = ▶[f](𝗱n◗p).
+lemma unwind2_rmap_rcons (f) (p) (l):
+      ▶[▶[f]p]l = ▶[f](p◖l).
 // qed.
 
-lemma unwind2_rmap_m_sn (f) (p):
-      ▶[f]p = ▶[f](𝗺◗p).
+lemma unwind2_rmap_d_dx (f) (p) (k:pnat):
+      ▶[f]p∘𝐮❨k❩ = ▶[f](p◖𝗱k).
 // qed.
 
-lemma unwind2_rmap_L_sn (f) (p):
-      (⫯▶[f]p) = ▶[f](𝗟◗p).
+lemma unwind2_rmap_m_dx (f) (p):
+      ▶[f]p = ▶[f](p◖𝗺).
 // qed.
 
-lemma unwind2_rmap_A_sn (f) (p):
-      ▶[f]p = ▶[f](𝗔◗p).
+lemma unwind2_rmap_L_dx (f) (p):
+      (⫯▶[f]p) = ▶[f](p◖𝗟).
 // qed.
 
-lemma unwind2_rmap_S_sn (f) (p):
-      ▶[f]p = ▶[f](𝗦◗p).
+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 list_append *******************************************)
-
-lemma unwind2_rmap_append (f) (p1) (p2):
-      ▶[▶[f]p2]p1 = ▶[f](p1●p2).
-#f #p1 elim p1 -p1 //
-* [ #n ] #p1 #IH #p2 //
-[ <unwind2_rmap_m_sn <unwind2_rmap_m_sn //
-| <unwind2_rmap_L_sn <unwind2_rmap_L_sn //
-| <unwind2_rmap_A_sn <unwind2_rmap_A_sn //
-| <unwind2_rmap_S_sn <unwind2_rmap_S_sn //
-]
+(* 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 list_rcons ********************************************)
+(* Constructions with path_lcons ********************************************)
 
-lemma unwind2_rmap_d_dx (f) (p) (n:pnat):
-      ▶[f∘𝐮❨n❩]p = ▶[f](p◖𝗱n).
+lemma unwind2_rmap_lcons (f) (p) (l):
+      ▶[▶[f]l]p = ▶[f](l◗p).
 // qed.
 
-lemma unwind2_rmap_m_dx (f) (p):
-      ▶[f]p = ▶[f](p◖𝗺).
+lemma unwind2_rmap_d_sn (f) (p) (k:pnat):
+      ▶[f∘𝐮❨k❩]p = ▶[f](𝗱k◗p).
 // qed.
 
-lemma unwind2_rmap_L_dx (f) (p):
-      ▶[⫯f]p = ▶[f](p◖𝗟).
+lemma unwind2_rmap_m_sn (f) (p):
+      ▶[f]p = ▶[f](𝗺◗p).
 // qed.
 
-lemma unwind2_rmap_A_dx (f) (p):
-      ▶[f]p = ▶[f](p◖𝗔).
+lemma unwind2_rmap_L_sn (f) (p):
+      ▶[⫯f]p = ▶[f](𝗟◗p).
 // qed.
 
-lemma unwind2_rmap_S_dx (f) (p):
-      ▶[f]p = ▶[f](p◖𝗦).
+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
new file mode 100644
index 000000000..7fda762da
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/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/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_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
index 7ca7f175c..c075e2f25 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
@@ -13,30 +13,24 @@
 (**************************************************************************)
 
 include "delayed_updating/unwind/unwind2_rmap.ma".
+include "delayed_updating/unwind/preunwind2_rmap_eq.ma".
 include "ground/relocation/tr_uni_compose.ma".
-include "ground/relocation/tr_compose_eq.ma".
-include "ground/relocation/tr_pn_eq.ma".
 include "ground/arith/nat_rplus_pplus.ma".
 
-(* UNWIND MAP FOR PATH ******************************************************)
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
 
-(* Constructions with stream_eq *********************************************)
+(* Constructions with tr_map_eq *********************************************)
 
 lemma unwind2_rmap_eq_repl (p):
       stream_eq_repl … (λf1,f2. ▶[f1]p ≗ ▶[f2]p).
 #p elim p -p //
-* [ #n ] #p #IH #f1 #f2 #Hf
-[ /3 width=1 by tr_compose_eq_repl/
-| /2 width=1 by/
-| /3 width=1 by tr_push_eq_repl/
-| /2 width=1 by/
-| /2 width=1 by/
-]
+#l #p #IH #f1 #f2 #Hf
+/3 width=1 by preunwind2_rmap_eq_repl/
 qed-.
 
-lemma tls_unwind2_rmap_d_sn (f) (p) (m) (n):
-      ⇂*[m+n]▶[f]p ≗ ⇂*[m]▶[f](𝗱n◗p).
-#f #p #m #n
-<unwind2_rmap_d_sn >nrplus_inj_dx
+lemma tls_unwind2_rmap_d_dx (f) (p) (n) (k):
+      ⇂*[n+k]▶[f]p ≗ ⇂*[n]▶[f](p◖𝗱k).
+#f #p #n #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_head.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
index f6fbae181..853f07e9c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
@@ -19,45 +19,45 @@ include "ground/relocation/xap.ma".
 include "ground/lib/stream_eq_eq.ma".
 include "ground/arith/nat_le_plus.ma".
 
-(* UNWIND MAP FOR PATH ******************************************************)
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
 
 (* Constructions with path_head *********************************************)
 
-lemma unwind2_rmap_head_xap_le_closed (f) (p) (q) (n) (k):
-      p = ↳[n]p → k ≤ n →
-      ▶[f](p●q)＠❨k❩ = ▶[f]↳[n](p●q)＠❨k❩.
-#f #p elim p -p
-[ #q #n #k #Hq
-  <(eq_inv_path_empty_head … Hq) -n #Hk
-  <(nle_inv_zero_dx … Hk) -k //
-| #l #p #IH #q #n @(nat_ind_succ … n) -n
-  [ #k #_ #Hk <(nle_inv_zero_dx … Hk) -k -IH //
-  | #n #_ #k cases l [ #m ]
-    [ <path_head_d_sn #Hq #Hk
+lemma unwind2_rmap_head_xap_le_closed (f) (p) (q) (n) (m):
+      q = ↳[n]q → m ≤ n →
+      ▶[f](p●q)＠❨m❩ = ▶[f]↳[n](p●q)＠❨m❩.
+#f #p #q elim q -q
+[ #n #m #Hq
+  <(eq_inv_path_empty_head … Hq) -n #Hm
+  <(nle_inv_zero_dx … Hm) -m //
+| #l #q #IH #n @(nat_ind_succ … n) -n
+  [ #m #_ #Hm <(nle_inv_zero_dx … Hm) -m -IH //
+  | #n #_ #m cases l [ #k ]
+    [ <path_head_d_dx #Hq #Hm
       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
-      <unwind2_rmap_d_sn <unwind2_rmap_d_sn
+      <unwind2_rmap_d_dx <unwind2_rmap_d_dx
       <tr_compose_xap <tr_compose_xap
       @(IH … Hq) -IH -Hq (**) (* auto too slow *)
       @nle_trans [| @tr_uni_xap ]
       /2 width=1 by nle_plus_bi_dx/
-    | <path_head_m_sn #Hq #Hk
+    | <path_head_m_dx #Hq #Hm
       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
-      <unwind2_rmap_m_sn <unwind2_rmap_m_sn
+      <unwind2_rmap_m_dx <unwind2_rmap_m_dx
       /2 width=2 by/
-    | <path_head_L_sn #Hq
-      @(nat_ind_succ … k) -k // #k #_ #Hk
-      lapply (nle_inv_succ_bi … Hk) -Hk #Hk
+    | <path_head_L_dx #Hq
+      @(nat_ind_succ … m) -m // #m #_ #Hm
+      lapply (nle_inv_succ_bi … Hm) -Hm #Hm
       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
-      <unwind2_rmap_L_sn <unwind2_rmap_L_sn
+      <unwind2_rmap_L_dx <unwind2_rmap_L_dx
       <tr_xap_push <tr_xap_push
       /3 width=2 by eq_f/
-    | <path_head_A_sn #Hq #Hk
+    | <path_head_A_dx #Hq #Hm
       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
-      <unwind2_rmap_A_sn <unwind2_rmap_A_sn
+      <unwind2_rmap_A_dx <unwind2_rmap_A_dx
       /2 width=2 by/
-    | <path_head_S_sn #Hq #Hk
+    | <path_head_S_dx #Hq #Hm
       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
-      <unwind2_rmap_S_sn <unwind2_rmap_S_sn
+      <unwind2_rmap_S_dx <unwind2_rmap_S_dx
       /2 width=2 by/
     ]
   ]
@@ -65,7 +65,7 @@ lemma unwind2_rmap_head_xap_le_closed (f) (p) (q) (n) (k):
 qed-.
 
 lemma unwind2_rmap_head_xap_closed (f) (p) (q) (n):
-      p = ↳[n]p →
+      q = ↳[n]q →
       ▶[f](p●q)＠❨n❩ = ▶[f]↳[n](p●q)＠❨n❩.
 /2 width=2 by unwind2_rmap_head_xap_le_closed/
 qed-.
@@ -76,58 +76,59 @@ lemma unwind2_rmap_head_xap (f) (p) (n):
 [ #n <path_head_empty <unwind2_rmap_labels_L <height_labels_L
   <tr_xap_pushs_le //
 | #l #p #IH #n @(nat_ind_succ … n) -n //
-  #n #_ cases l [ #m ]
-  [ <unwind2_rmap_d_sn <path_head_d_sn <height_d_sn
-    <nplus_assoc >IH -IH <tr_compose_xap <tr_uni_xap_succ //
-  | <unwind2_rmap_m_sn <path_head_m_sn <height_m_sn //
-  | <unwind2_rmap_L_sn <path_head_L_sn <height_L_sn
-    <tr_xap_push <npred_succ //
-  | <unwind2_rmap_A_sn <path_head_A_sn <height_A_sn //
-  | <unwind2_rmap_S_sn <path_head_S_sn <height_S_sn //
+  #n #_ cases l [ #k ]
+  [ <unwind2_rmap_d_dx <path_head_d_dx <height_d_dx
+    <nplus_comm in ⊢ (??(??%)?); <nplus_assoc
+    >IH -IH <tr_compose_xap <tr_uni_xap_succ //
+  | <unwind2_rmap_m_dx <path_head_m_dx <height_m_dx //
+  | <unwind2_rmap_L_dx <path_head_L_dx <height_L_dx
+    <tr_xap_push <npred_succ <nplus_succ_sn //
+  | <unwind2_rmap_A_dx <path_head_A_dx <height_A_dx //
+  | <unwind2_rmap_S_dx <path_head_S_dx <height_S_dx //
   ]
 ]
 qed.
 
 lemma unwind2_rmap_append_pap_closed (f) (p) (q) (n:pnat):
-      p = ↳[n]p →
-      ♭p = ninj (▶[f](p●q)＠⧣❨n❩).
+      q = ↳[n]q →
+      ♭q = ninj (▶[f](p●q)＠⧣❨n❩).
 #f #p #q #n #Hn
->tr_xap_ninj >(path_head_refl_append q … Hn) in ⊢ (??%?); 
+>tr_xap_ninj >(path_head_refl_append p … Hn) in ⊢ (??%?);
 >(unwind2_rmap_head_xap_closed … Hn) -Hn
 <path_head_depth //
 qed.
 
-lemma tls_unwind2_rmap_plus_closed (f) (p) (q) (n) (k):
-      p = ↳[n]p →
-      ⇂*[k]▶[f]q ≗ ⇂*[n+k]▶[f](p●q).
-#f #p elim p -p
-[ #q #n #k #Hq
+lemma tls_unwind2_rmap_plus_closed (f) (p) (q) (n) (m):
+      q = ↳[n]q →
+      ⇂*[m]▶[f]p ≗ ⇂*[n+m]▶[f](p●q).
+#f #p #q elim q -q
+[ #n #m #Hq
   <(eq_inv_path_empty_head … Hq) -n //
-| #l #p #IH #q #n @(nat_ind_succ … n) -n //
-  #n #_ #k cases l [ #m ]
-  [ <path_head_d_sn #Hq
+| #l #q #IH #n @(nat_ind_succ … n) -n //
+  #n #_ #m cases l [ #k ]
+  [ <path_head_d_dx #Hq
     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq <nrplus_inj_sn
-    @(stream_eq_trans … (tls_unwind2_rmap_d_sn …))
+    @(stream_eq_trans … (tls_unwind2_rmap_d_dx …))
     >nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn <nplus_plus_comm_23
     /2 width=1 by/
-  | <path_head_m_sn #Hq
+  | <path_head_m_dx #Hq
     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
     <unwind2_rmap_m_sn /2 width=1 by/
-  | <path_head_L_sn #Hq
+  | <path_head_L_dx #Hq
     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
-    <unwind2_rmap_L_sn <nplus_succ_sn /2 width=1 by/
-  | <path_head_A_sn #Hq
+    <unwind2_rmap_L_dx <nplus_succ_sn /2 width=1 by/
+  | <path_head_A_dx #Hq
     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
-    <unwind2_rmap_A_sn /2 width=2 by/
-  | <path_head_S_sn #Hq
+    <unwind2_rmap_A_dx /2 width=2 by/
+  | <path_head_S_dx #Hq
     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
-    <unwind2_rmap_S_sn /2 width=2 by/
+    <unwind2_rmap_S_dx /2 width=2 by/
   ]
 ]
 qed-.
 
 lemma tls_unwind2_rmap_closed (f) (p) (q) (n):
-      p = ↳[n]p →
-      ▶[f]q ≗ ⇂*[n]▶[f](p●q).
+      q = ↳[n]q →
+      ▶[f]p ≗ ⇂*[n]▶[f](p●q).
 /2 width=1 by tls_unwind2_rmap_plus_closed/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_labels.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_labels.ma
index b1ddacd6f..d139018f7 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_labels.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_labels.ma
@@ -16,7 +16,7 @@ include "delayed_updating/unwind/unwind2_rmap.ma".
 include "delayed_updating/syntax/path_labels.ma".
 include "ground/relocation/tr_pushs.ma".
 
-(* UNWIND MAP FOR PATH ******************************************************)
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
 
 (* Constructions with labels ************************************************)
 
@@ -24,5 +24,5 @@ lemma unwind2_rmap_labels_L (f) (n):
       (⫯*[n]f) = ▶[f](𝗟∗∗n).
 #f #n @(nat_ind_succ … n) -n //
 #n #IH
-<labels_succ <unwind2_rmap_L_sn //
+<labels_succ <unwind2_rmap_L_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
new file mode 100644
index 000000000..02c51eca2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/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/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):
+      ↑[⊗p]g∘▶[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∘↑[p]f ≗ ▶[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
index 6a52ef2e5..0d949e3b5 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_structure.ma
@@ -17,15 +17,16 @@ include "delayed_updating/syntax/path_structure.ma".
 include "delayed_updating/syntax/path_depth.ma".
 include "ground/relocation/tr_pushs.ma".
 
-(* UNWIND MAP FOR PATH ******************************************************)
+(* TAILED UNWIND FOR RELOCATION MAP *****************************************)
 
 (* Constructions with structure and depth ***********************************)
 
-lemma unwind2_rmap_structure (p) (f):
+lemma unwind2_rmap_structure (f) (p):
       (⫯*[♭p]f) = ▶[f]⊗p.
-#p elim p -p //
-* [ #n ] #p #IH #f //
-[ <unwind2_rmap_A_sn //
-| <unwind2_rmap_S_sn //
+#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/unwind_gen.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma
deleted file mode 100644
index 0ea3ab8ac..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma
+++ /dev/null
@@ -1,86 +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/path.ma".
-include "delayed_updating/notation/functions/black_diamond_2.ma".
-include "ground/relocation/tr_pap.ma".
-
-(* GENERIC UNWIND FOR PATH **************************************************)
-
-rec definition unwind_gen (f) (p) on p ≝
-match p with
-[ list_empty     ⇒ 𝐞
-| list_lcons l q ⇒
-  match l with
-  [ label_d n ⇒
-    match q with
-    [ list_empty     ⇒ 𝗱(f＠⧣❨n❩)◗(unwind_gen f q)
-    | list_lcons _ _ ⇒ unwind_gen f q
-    ]
-  | label_m   ⇒ unwind_gen f q
-  | label_L   ⇒ l◗(unwind_gen f q)
-  | label_A   ⇒ l◗(unwind_gen f q)
-  | label_S   ⇒ l◗(unwind_gen f q)
-  ]
-].
-
-interpretation
-  "generic unwind (path)"
-  'BlackDiamond f p = (unwind_gen f p).
-
-(* Basic constructions ******************************************************)
-
-lemma unwind_gen_empty (f):
-      (𝐞) = ◆[f]𝐞.
-// qed.
-
-lemma unwind_gen_d_empty (f) (n):
-      𝗱(f＠⧣❨n❩)◗𝐞 = ◆[f](𝗱n◗𝐞).
-// qed.
-
-lemma unwind_gen_d_lcons (f) (p) (l) (n):
-      ◆[f](l◗p) = ◆[f](𝗱n◗l◗p).
-// qed.
-
-lemma unwind_gen_m_sn (f) (p):
-      ◆[f]p = ◆[f](𝗺◗p).
-// qed.
-
-lemma unwind_gen_L_sn (f) (p):
-      (𝗟◗◆[f]p) = ◆[f](𝗟◗p).
-// qed.
-
-lemma unwind_gen_A_sn (f) (p):
-      (𝗔◗◆[f]p) = ◆[f](𝗔◗p).
-// qed.
-
-lemma unwind_gen_S_sn (f) (p):
-      (𝗦◗◆[f]p) = ◆[f](𝗦◗p).
-// qed.
-
-(* Advanced eliminations with path ******************************************)
-
-lemma path_ind_unwind (Q:predicate …):
-      Q (𝐞) →
-      (∀n. Q (𝐞) → Q (𝗱n◗𝐞)) →
-      (∀n,l,p. Q (l◗p) → Q (𝗱n◗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
-elim p -p [| * [ #n * ] ]
-/2 width=1 by/
-qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
deleted file mode 100644
index 5c92a9af5..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
+++ /dev/null
@@ -1,269 +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/unwind_gen.ma".
-include "delayed_updating/syntax/path_structure.ma".
-include "delayed_updating/syntax/path_inner.ma".
-include "delayed_updating/syntax/path_proper.ma".
-include "ground/xoa/ex_4_2.ma".
-include "ground/xoa/ex_3_2.ma".
-
-(* GENERIC UNWIND FOR PATH **************************************************)
-
-(* Basic constructions with structure ***************************************)
-
-lemma structure_unwind_gen (p) (f):
-      ⊗p = ⊗◆[f]p.
-#p @(path_ind_unwind … p) -p //
-qed.
-
-lemma unwind_gen_structure (p) (f):
-      ⊗p = ◆[f]⊗p.
-#p @(path_ind_unwind … p) -p //
-qed.
-
-(* Destructions with structure **********************************************)
-
-lemma unwind_gen_des_structure (q) (p) (f):
-      ⊗q = ◆[f]p → ⊗q = ⊗p.
-// qed-.
-
-(* Constructions with proper condition for path *****************************)
-
-lemma unwind_gen_append_proper_dx (p2) (p1) (f): p2 ϵ 𝐏 →
-      (⊗p1)●(◆[f]p2) = ◆[f](p1●p2).
-#p2 #p1 @(path_ind_unwind … p1) -p1 //
-[ #n | #n #l #p1 |*: #p1 ] #IH #f #Hp2
-[ elim (ppc_inv_lcons … Hp2) -Hp2 #l #q #H0 destruct //
-| <unwind_gen_d_lcons <IH //
-| <unwind_gen_m_sn <IH //
-| <unwind_gen_L_sn <IH //
-| <unwind_gen_A_sn <IH //
-| <unwind_gen_S_sn <IH //
-]
-qed-.
-
-(* Constructions with inner condition for path ******************************)
-
-lemma unwind_gen_append_inner_sn (p1) (p2) (f): p1 ϵ 𝐈 →
-      (⊗p1)●(◆[f]p2) = ◆[f](p1●p2).
-#p1 @(list_ind_rcons … p1) -p1 //
-#p1 * [ #n ] #_ #p2 #f #Hp1
-[ elim (pic_inv_d_dx … Hp1)
-| <list_append_rcons_sn <unwind_gen_append_proper_dx //
-| <list_append_rcons_sn <unwind_gen_append_proper_dx //
-  <structure_L_dx <list_append_rcons_sn //
-| <list_append_rcons_sn <unwind_gen_append_proper_dx //
-  <structure_A_dx <list_append_rcons_sn //
-| <list_append_rcons_sn <unwind_gen_append_proper_dx //
-  <structure_S_dx <list_append_rcons_sn //
-]
-qed-.
-
-(* Advanced constructions with list_rcons ***********************************)
-
-lemma unwind_gen_d_dx (f) (p) (n):
-      (⊗p)◖𝗱(f＠⧣❨n❩) = ◆[f](p◖𝗱n).
-#f #p #n <unwind_gen_append_proper_dx //
-qed.
-
-lemma unwind_gen_m_dx (f) (p):
-      ⊗p = ◆[f](p◖𝗺).
-#f #p <unwind_gen_append_proper_dx //
-qed.
-
-lemma unwind_gen_L_dx (f) (p):
-      (⊗p)◖𝗟 = ◆[f](p◖𝗟).
-#f #p <unwind_gen_append_proper_dx //
-qed.
-
-lemma unwind_gen_A_dx (f) (p):
-      (⊗p)◖𝗔 = ◆[f](p◖𝗔).
-#f #p <unwind_gen_append_proper_dx //
-qed.
-
-lemma unwind_gen_S_dx (f) (p):
-      (⊗p)◖𝗦 = ◆[f](p◖𝗦).
-#f #p <unwind_gen_append_proper_dx //
-qed.
-
-lemma unwind_gen_root (f) (p):
-      ∃∃r. 𝐞 = ⊗r & ⊗p●r = ◆[f]p.
-#f #p @(list_ind_rcons … p) -p
-[ /2 width=3 by ex2_intro/
-| #p * [ #n ] /2 width=3 by ex2_intro/
-]
-qed-.
-
-(* Advanced inversions ******************************************************)
-
-lemma unwind_gen_inv_d_sn (k) (q) (p) (f):
-      (𝗱k◗q) = ◆[f]p →
-      ∃∃r,h. 𝐞 = ⊗r & f＠⧣❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
-#k #q #p @(path_ind_unwind … p) -p
-[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
-[ <unwind_gen_empty #H destruct
-| <unwind_gen_d_empty #H destruct -IH
-  /2 width=5 by ex4_2_intro/
-| <unwind_gen_d_lcons #H
-  elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
-  /2 width=5 by ex4_2_intro/
-| <unwind_gen_m_sn #H
-  elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
-  /2 width=5 by ex4_2_intro/
-| <unwind_gen_L_sn #H destruct
-| <unwind_gen_A_sn #H destruct
-| <unwind_gen_S_sn #H destruct
-]
-qed-.
-
-lemma unwind_gen_inv_m_sn (q) (p) (f):
-      (𝗺◗q) = ◆[f]p → ⊥.
-#q #p @(path_ind_unwind … p) -p
-[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
-[ <unwind_gen_empty #H destruct
-| <unwind_gen_d_empty #H destruct
-| <unwind_gen_d_lcons #H /2 width=2 by/
-| <unwind_gen_m_sn #H /2 width=2 by/
-| <unwind_gen_L_sn #H destruct
-| <unwind_gen_A_sn #H destruct
-| <unwind_gen_S_sn #H destruct
-]
-qed-.
-
-lemma unwind_gen_inv_L_sn (q) (p) (f):
-      (𝗟◗q) = ◆[f]p →
-      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ◆[f]r2 & r1●𝗟◗r2 = p.
-#q #p @(path_ind_unwind … p) -p
-[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
-[ <unwind_gen_empty #H destruct
-| <unwind_gen_d_empty #H destruct
-| <unwind_gen_d_lcons #H
-  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
-  /2 width=5 by ex3_2_intro/
-| <unwind_gen_m_sn #H
-  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
-  /2 width=5 by ex3_2_intro/
-| <unwind_gen_L_sn #H destruct -IH
-  /2 width=5 by ex3_2_intro/
-| <unwind_gen_A_sn #H destruct
-| <unwind_gen_S_sn #H destruct
-]
-qed-.
-
-lemma unwind_gen_inv_A_sn (q) (p) (f):
-      (𝗔◗q) = ◆[f]p →
-      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ◆[f]r2 & r1●𝗔◗r2 = p.
-#q #p @(path_ind_unwind … p) -p
-[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
-[ <unwind_gen_empty #H destruct
-| <unwind_gen_d_empty #H destruct
-| <unwind_gen_d_lcons #H
-  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
-  /2 width=5 by ex3_2_intro/
-| <unwind_gen_m_sn #H
-  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
-  /2 width=5 by ex3_2_intro/
-| <unwind_gen_L_sn #H destruct
-| <unwind_gen_A_sn #H destruct -IH
-  /2 width=5 by ex3_2_intro/
-| <unwind_gen_S_sn #H destruct
-]
-qed-.
-
-lemma unwind_gen_inv_S_sn (q) (p) (f):
-      (𝗦◗q) = ◆[f]p →
-      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ◆[f]r2 & r1●𝗦◗r2 = p.
-#q #p @(path_ind_unwind … p) -p
-[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
-[ <unwind_gen_empty #H destruct
-| <unwind_gen_d_empty #H destruct
-| <unwind_gen_d_lcons #H
-  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
-  /2 width=5 by ex3_2_intro/
-| <unwind_gen_m_sn #H
-  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
-  /2 width=5 by ex3_2_intro/| <unwind_gen_L_sn #H destruct
-| <unwind_gen_A_sn #H destruct
-| <unwind_gen_S_sn #H destruct -IH
-  /2 width=5 by ex3_2_intro/
-]
-qed-.
-
-(* Inversions with proper condition for path ********************************)
-
-lemma unwind_gen_inv_append_proper_dx (q2) (q1) (p) (f):
-      q2 ϵ 𝐏 → q1●q2 = ◆[f]p →
-      ∃∃p1,p2. ⊗p1 = q1 & ◆[f]p2 = q2 & p1●p2 = p.
-#q2 #q1 elim q1 -q1
-[ #p #f #Hq2 <list_append_empty_sn #H destruct
-  /2 width=5 by ex3_2_intro/
-| * [ #n1 ] #q1 #IH #p #f #Hq2 <list_append_lcons_sn #H
-  [ elim (unwind_gen_inv_d_sn … H) -H #r1 #m1 #_ #_ #H0 #_ -IH
-    elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
-    elim Hq2 -Hq2 //
-  | elim (unwind_gen_inv_m_sn … H)
-  | elim (unwind_gen_inv_L_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
-    elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
-    @(ex3_2_intro … (r1●𝗟◗p1)) //
-    <structure_append <Hr1 -Hr1 //
-  | elim (unwind_gen_inv_A_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
-    elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
-    @(ex3_2_intro … (r1●𝗔◗p1)) //
-    <structure_append <Hr1 -Hr1 //
-  | elim (unwind_gen_inv_S_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
-    elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
-    @(ex3_2_intro … (r1●𝗦◗p1)) //
-    <structure_append <Hr1 -Hr1 //
-  ]
-]
-qed-.
-
-(* Inversions with inner condition for path *********************************)
-
-lemma unwind_gen_inv_append_inner_sn (q1) (q2) (p) (f):
-      q1 ϵ 𝐈 → q1●q2 = ◆[f]p →
-      ∃∃p1,p2. ⊗p1 = q1 & ◆[f]p2 = q2 & p1●p2 = p.
-#q1 @(list_ind_rcons … q1) -q1
-[ #q2 #p #f #Hq1 <list_append_empty_sn #H destruct
-  /2 width=5 by ex3_2_intro/
-| #q1 * [ #n1 ] #_ #q2 #p #f #Hq2
-  [ elim (pic_inv_d_dx … Hq2)
-  | <list_append_rcons_sn #H0
-    elim (unwind_gen_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
-    elim (unwind_gen_inv_m_sn … (sym_eq … H2))
-  | <list_append_rcons_sn #H0
-    elim (unwind_gen_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
-    elim (unwind_gen_inv_L_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
-    @(ex3_2_intro … (p1●r2◖𝗟)) [1,3: // ]
-    [ <structure_append <structure_L_dx <Hr2 -Hr2 //
-    | <list_append_assoc <list_append_rcons_sn //
-    ]
-  | <list_append_rcons_sn #H0
-    elim (unwind_gen_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
-    elim (unwind_gen_inv_A_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
-    @(ex3_2_intro … (p1●r2◖𝗔)) [1,3: // ]
-    [ <structure_append <structure_A_dx <Hr2 -Hr2 //
-    | <list_append_assoc <list_append_rcons_sn //
-    ]
-  | <list_append_rcons_sn #H0
-    elim (unwind_gen_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
-    elim (unwind_gen_inv_S_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
-    @(ex3_2_intro … (p1●r2◖𝗦)) [1,3: // ]
-    [ <structure_append <structure_S_dx <Hr2 -Hr2 //
-    | <list_append_assoc <list_append_rcons_sn //
-    ]
-  ]
-]
-qed-.
-- 
2.39.2