From 97ff918432e878ab8314c72fe2b948a253b26e21 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 21 May 2022 20:23:22 +0200
Subject: [PATCH] update in delayed_updating

+ unwind completed with an important result on lift
---
 .../unwind.ma => etc/unwind1/unwind.etc}      |   0
 .../unwind1/unwind_constructors.etc}          |   0
 .../unwind1/unwind_depth.etc}                 |   0
 .../unwind1/unwind_eq.etc}                    |   0
 .../unwind1/unwind_eq_etc.etc}                |   0
 .../unwind1/unwind_fsubst.etc}                |   0
 .../unwind1/unwind_preterm_eq.etc}            |   0
 .../unwind1/unwind_prototerm.etc}             |   0
 .../unwind1/unwind_prototerm_eq.etc}          |   0
 .../unwind1/unwind_structure.etc}             |   0
 .../unwind1/unwind_structure_depth.etc}       |   0
 .../unwind1/unwind_update.etc}                |   0
 .../delayed_updating/substitution/lift_eq.ma  |  43 ++++++-
 .../delayed_updating/syntax/bdd_term.ma       |   2 +-
 .../delayed_updating/syntax/path_proper.ma    |   8 ++
 .../delayed_updating/unwind/nap.ma            |   1 -
 .../unwind/unwind2_constructors.ma            |  39 ++++++
 .../delayed_updating/unwind/unwind2_path.ma   |  84 +++++++++++++
 .../unwind/unwind2_path_eq.ma                 |  40 ++++++
 .../unwind/unwind2_path_lift.ma               |  31 +++++
 .../unwind/unwind2_path_structure.ma          | 116 ++++++++++++++++++
 .../unwind/unwind2_preterm_eq.ma              |  67 ++++++++++
 .../unwind/unwind2_preterm_fsubst.ma          |  62 ++++++++++
 .../unwind/unwind2_prototerm.ma               |  30 +++++
 .../unwind/unwind2_prototerm_eq.ma            |  41 +++++++
 .../unwind/unwind2_prototerm_lift.ma          |  31 +++++
 .../unwind/unwind2_rmap_head.ma               |  55 +++++++--
 .../delayed_updating/unwind/unwind_gen.ma     |   4 +-
 .../unwind/unwind_gen_after.ma                |   3 +-
 .../delayed_updating/unwind/unwind_gen_eq.ma  |  12 +-
 .../unwind/unwind_gen_structure.ma            |  24 ++--
 .../delayed_updating/unwind/xap.ma            |  55 +++++++++
 32 files changed, 710 insertions(+), 38 deletions(-)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind1/unwind.ma => etc/unwind1/unwind.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind1/unwind_constructors.ma => etc/unwind1/unwind_constructors.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind1/unwind_depth.ma => etc/unwind1/unwind_depth.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind1/unwind_eq.ma => etc/unwind1/unwind_eq.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind1/unwind_eq_etc.ma => etc/unwind1/unwind_eq_etc.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind1/unwind_fsubst.ma => etc/unwind1/unwind_fsubst.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind1/unwind_preterm_eq.ma => etc/unwind1/unwind_preterm_eq.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind1/unwind_prototerm.ma => etc/unwind1/unwind_prototerm.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind1/unwind_prototerm_eq.ma => etc/unwind1/unwind_prototerm_eq.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind1/unwind_structure.ma => etc/unwind1/unwind_structure.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind1/unwind_structure_depth.ma => etc/unwind1/unwind_structure_depth.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind1/unwind_update.ma => etc/unwind1/unwind_update.etc} (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_eq.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_structure.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_eq.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_eq.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/xap.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_constructors.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_constructors.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_constructors.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_depth.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_depth.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_depth.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_eq.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_eq.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_eq.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_eq_etc.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_eq_etc.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_eq_etc.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_eq_etc.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_fsubst.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_fsubst.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_fsubst.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_fsubst.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_preterm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_preterm_eq.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_preterm_eq.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_preterm_eq.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_prototerm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_prototerm.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_prototerm.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_prototerm.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_prototerm_eq.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_prototerm_eq.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_prototerm_eq.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_structure.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_structure.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_structure_depth.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_structure_depth.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_structure_depth.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_update.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_update.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_update.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind1/unwind_update.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
index 68a4ceb36..5eac1985e 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
@@ -13,11 +13,6 @@
 (**************************************************************************)
 
 include "delayed_updating/substitution/lift.ma".
-(*
-include "ground/relocation/tr_uni_compose.ma".
-include "ground/relocation/tr_compose_compose.ma".
-include "ground/relocation/tr_compose_eq.ma".
-*)
 include "ground/relocation/tr_pap_eq.ma".
 include "ground/relocation/tr_pn_eq.ma".
 include "ground/lib/stream_tls_eq.ma".
@@ -110,6 +105,44 @@ lemma lift_path_A_sn (f) (p):
 lemma lift_path_S_sn (f) (p):
       (𝗦◗↑[f]p) = ↑[f](𝗦◗p).
 // qed.
+
+lemma lift_path_append (p2) (p1) (f):
+      (↑[f]p1)●(↑[↑[p1]f]p2) = ↑[f](p1●p2).
+#p2 #p1 elim p1 -p1 //
+* [ #n1 ] #p1 #IH #f
+[ <lift_path_d_sn <lift_path_d_sn <IH //
+| <lift_path_m_sn <lift_path_m_sn <IH //
+| <lift_path_L_sn <lift_path_L_sn <IH //
+| <lift_path_A_sn <lift_path_A_sn <IH //
+| <lift_path_S_sn <lift_path_S_sn <IH //
+]
+qed.
+
+lemma lift_path_d_dx (f) (p) (n):
+      (↑[f]p)◖𝗱((↑[p]f)＠⧣❨n❩) = ↑[f](p◖𝗱n).
+#f #p #n <lift_path_append //
+qed.
+
+lemma lift_path_m_dx (f) (p):
+      (↑[f]p)◖𝗺 = ↑[f](p◖𝗺).
+#f #p <lift_path_append //
+qed.
+
+lemma lift_path_L_dx (f) (p):
+      (↑[f]p)◖𝗟 = ↑[f](p◖𝗟).
+#f #p <lift_path_append //
+qed.
+
+lemma lift_path_A_dx (f) (p):
+      (↑[f]p)◖𝗔 = ↑[f](p◖𝗔).
+#f #p <lift_path_append //
+qed.
+
+lemma lift_path_S_dx (f) (p):
+      (↑[f]p)◖𝗦 = ↑[f](p◖𝗦).
+#f #p <lift_path_append //
+qed.
+
 (* COMMENT 
 
 (* Advanced constructions with proj_rmap and stream_tls *********************)
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
index 9cfe28ad9..8aaefad91 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
@@ -27,7 +27,7 @@ inductive bdd: 𝒫❨prototerm❩ ≝
 | bdd_oref: ∀n. bdd (⧣n)
 | bdd_iref: ∀t,n. bdd t → bdd (𝛗n.t)
 | bdd_abst: ∀t. bdd t → bdd (𝛌.t)
-| bdd_appl: ∀u,t. bdd u → bdd t → bdd (@u.t)
+| bdd_appl: ∀u,t. bdd u → bdd t → bdd (＠u.t)
 | bdd_conv: ∀t1,t2. t1 ⇔ t2 → bdd t1 → bdd t2
 .
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma
index 66de8a4f6..9cab60b87 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_proper.ma
@@ -47,3 +47,11 @@ lemma ppc_inv_lcons (p):
 | #l #q #_ /2 width=3 by ex1_2_intro/
 ]
 qed-.
+
+lemma ppc_inv_rcons (p):
+      p ϵ 𝐏 → ∃∃q,l. q◖l = p.
+#p @(list_ind_rcons … p) -p
+[ #H0 elim (ppc_inv_empty … H0)
+| #q #l #_ #_ /2 width=3 by ex1_2_intro/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/nap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/nap.ma
index bfa89a784..985b3ae26 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/nap.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/nap.ma
@@ -1,6 +1,5 @@
 include "ground/relocation/tr_uni_pap.ma".
 include "ground/relocation/tr_compose_pap.ma".
-include "ground/relocation/tr_pap_pn.ma".
 include "ground/notation/functions/applysucc_2.ma".
 include "ground/arith/nat_lt.ma".
 include "ground/arith/nat_plus_rplus.ma".
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma
new file mode 100644
index 000000000..c70e09e1a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_constructors.ma
@@ -0,0 +1,39 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "delayed_updating/unwind/unwind2_prototerm_eq.ma".
+include "delayed_updating/syntax/prototerm_constructors.ma".
+
+(* 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))
+/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
+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).
+/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
new file mode 100644
index 000000000..3288fc734
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path.ma
@@ -0,0 +1,84 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/unwind/unwind2_rmap.ma".
+include "delayed_updating/syntax/path_reverse.ma".
+include "delayed_updating/notation/functions/black_downtriangle_2.ma".
+include "ground/lib/list_tl.ma".
+
+(* UNWIND FOR PATH **********************************************************)
+
+definition unwind2_path (f) (p): path ≝
+           ◆[▶[f]⇂(pᴿ)]p
+.
+
+interpretation
+  "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◗𝐞).
+// 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_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_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_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 //
+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 //
+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
new file mode 100644
index 000000000..cb0826a0b
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_eq.ma
@@ -0,0 +1,40 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "delayed_updating/unwind/unwind2_path.ma".
+include "delayed_updating/unwind/unwind2_rmap_eq.ma".
+include "delayed_updating/unwind/unwind_gen_eq.ma".
+include "ground/relocation/tr_compose_compose.ma".
+include "ground/relocation/tr_compose_pn.ma".
+
+(* UNWIND FOR PATH **********************************************************)
+
+(* Constructions with stream_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/
+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
new file mode 100644
index 000000000..642056c89
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma
@@ -0,0 +1,31 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "delayed_updating/unwind/unwind2_path_eq.ma".
+include "delayed_updating/substitution/lift_eq.ma".
+include "ground/relocation/tr_uni_compose.ma".
+
+(* UNWIND FOR PATH **********************************************************)
+
+(* Properties with lift_path ************************************************)
+
+lemma unwind2_lift_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 //
+]
+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
new file mode 100644
index 000000000..7cb6190b1
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_structure.ma
@@ -0,0 +1,116 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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".
+include "delayed_updating/syntax/path_inner.ma".
+include "delayed_updating/syntax/path_proper.ma".
+include "ground/xoa/ex_4_2.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-.
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
new file mode 100644
index 000000000..9ceccc0e2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_eq.ma
@@ -0,0 +1,67 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "delayed_updating/unwind/unwind2_prototerm.ma".
+include "delayed_updating/unwind/unwind2_path_structure.ma".
+include "delayed_updating/syntax/preterm.ma".
+include "delayed_updating/syntax/path_structure_inner.ma".
+include "ground/lib/subset_equivalence.ma".
+
+(* UNWIND FOR PRETERM *******************************************************)
+
+(* Constructions with subset_equivalence ************************************)
+
+lemma unwind2_term_grafted_sn (f) (t) (p): p ϵ 𝐈 →
+      ▼[▶[f]pᴿ](t⋔p) ⊆ (▼[f]t)⋔(⊗p).
+#f #t #p #Hp #q * #r #Hr #H0 destruct
+@(ex2_intro … Hr) -Hr
+<unwind2_path_append_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 #H1p #H2p #Ht #q * #r #Hr #H0
+elim (unwind2_path_inv_append_inner_sn … (sym_eq … H0)) -H0 //
+#p0 #q0 #Hp0 #Hq0 #H0 destruct
+<(Ht … Hp0) [|*: /2 width=2 by ex_intro/ ] -p
+/2 width=1 by in_comp_unwind2_path_term/
+qed-.
+
+lemma unwind2_term_grafted (f) (t) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
+      ▼[▶[f]pᴿ](t⋔p) ⇔ (▼[f]t)⋔(⊗p).
+/3 width=1 by unwind2_term_grafted_sn, unwind2_term_grafted_dx, conj/ qed.
+
+lemma unwind2_term_grafted_S_dx (f) (t) (p): p ϵ ▵t → t ϵ 𝐓 →
+      (▼[f]t)⋔((⊗p)◖𝗦) ⊆ ▼[▶[f]pᴿ](t⋔(p◖𝗦)).
+#f #t #p #Hp #Ht #q * #r #Hr
+<list_append_rcons_sn #H0
+elim (unwind2_path_inv_append_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
+#r1 #r2 #Hr1 #Hr2 #H0 destruct
+lapply (preterm_in_root_append_inv_structure_empty_dx … p0 … Ht Hr1)
+[ /2 width=2 by ex_intro/ ] -Hr1 #Hr1 destruct
+/2 width=1 by in_comp_unwind2_path_term/
+qed-.
+
+lemma unwind2_term_grafted_S (f) (t) (p): p ϵ ▵t → t ϵ 𝐓 →
+      ▼[▶[f]pᴿ](t⋔(p◖𝗦)) ⇔ (▼[f]t)⋔((⊗p)◖𝗦).
+#f #t #p #Hp #Ht
+@conj
+[ >unwind2_rmap_S_sn >reverse_rcons >structure_S_dx
+  @unwind2_term_grafted_sn // (**) (* auto fails *)
+| /2 width=1 by unwind2_term_grafted_S_dx/
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma
new file mode 100644
index 000000000..4245a6638
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma
@@ -0,0 +1,62 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "delayed_updating/unwind/unwind2_prototerm_eq.ma".
+include "delayed_updating/unwind/unwind2_path_structure.ma".
+include "delayed_updating/substitution/fsubst.ma".
+include "delayed_updating/syntax/preterm.ma".
+include "delayed_updating/syntax/prototerm_proper.ma".
+
+(* 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 #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_ppc_comp_trans, or_introl, ex2_intro/
+| * #q #Hq #H1 #H0
+  @(ex2_intro … H1) @or_intror @conj // *
+  [ <list_append_empty_dx #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/ ]
+  ]
+]
+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 #u #p #Hu #H1p #H2p #ql * #q * *
+[ #r #Hu #H1 #H2 destruct
+  @or_introl @ex2_intro
+  [|| <unwind2_path_append_proper_dx /2 width=5 by in_ppc_comp_trans/ ]
+  /2 width=3 by ex2_intro/
+| #Hq #H0 #H1 destruct
+  @or_intror @conj [ /2 width=1 by in_comp_unwind2_path_term/ ] *
+  [ <list_append_empty_dx #Hr @(H0 … (𝐞)) -H0
+    <list_append_empty_dx @H2p -H2p
+    /2 width=2 by unwind_gen_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/
+  ]
+]
+qed-.
+
+lemma unwind2_term_fsubst (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 𝐓 →
+      (▼[f]t)[⋔(⊗p)←▼[▶[f]pᴿ]u] ⇔ ▼[f](t[⋔p←u]).
+/4 width=3 by unwind2_term_fsubst_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
new file mode 100644
index 000000000..e0515c7f0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm.ma
@@ -0,0 +1,30 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "delayed_updating/unwind/unwind2_path.ma".
+include "delayed_updating/syntax/prototerm.ma".
+include "ground/lib/subset_ext.ma".
+
+(* UNWIND FOR PROTOTERM *****************************************************)
+
+interpretation
+  "unwind (prototerm)"
+  'BlackDownTriangle f t = (subset_ext_f1 ? ? (unwind2_path f) t).
+
+(* Basic constructions ******************************************************)
+
+lemma in_comp_unwind2_path_term (f) (p) (t):
+      p ϵ t → ▼[f]p ϵ ▼[f]t.
+/2 width=1 by subset_in_ext_f1_dx/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_eq.ma
new file mode 100644
index 000000000..dbde59810
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_eq.ma
@@ -0,0 +1,41 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(**) (* reverse include *)
+include "ground/lib/subset_ext_equivalence.ma".
+include "delayed_updating/unwind/unwind2_path_eq.ma".
+include "delayed_updating/unwind/unwind2_prototerm.ma".
+
+(* UNWIND FOR PROTOTERM *****************************************************)
+
+(* Constructions with subset_equivalence ************************************)
+
+lemma unwind2_term_eq_repl_sn (f1) (f2) (t):
+      f1 ≗ f2 → ▼[f1]t ⇔ ▼[f2]t.
+/3 width=1 by subset_equivalence_ext_f1_exteq, unwind2_path_eq_repl/
+qed.
+
+lemma unwind2_term_eq_repl_dx (f) (t1) (t2):
+      t1 ⇔ t2 → ▼[f]t1 ⇔ ▼[f]t2.
+/2 width=1 by subset_equivalence_ext_f1_bi/
+qed.
+
+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_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma
new file mode 100644
index 000000000..8e3d2cf2f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma
@@ -0,0 +1,31 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(**) (* reverse include *)
+include "ground/lib/subset_ext_equivalence.ma".
+include "delayed_updating/substitution/lift_prototerm.ma".
+include "delayed_updating/unwind/unwind2_path_lift.ma".
+include "delayed_updating/unwind/unwind2_prototerm.ma".
+
+(* UNWIND FOR PROTOTERM *****************************************************)
+
+(* Constructions with lift_prototerm ****************************************)
+
+lemma unwind2_lift_term_after (f1) (f2) (t):
+      ↑[f2]▼[f1]t ⇔ ▼[f2∘f1]t.
+#f1 #f2 #t @subset_eq_trans
+[| @subset_inclusion_ext_f1_compose ]
+@subset_equivalence_ext_f1_exteq #p
+@unwind2_lift_path_after
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
index 579cbd514..6b159e8c5 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
@@ -13,26 +13,67 @@
 (**************************************************************************)
 
 include "delayed_updating/unwind/unwind2_rmap_labels.ma".
-include "delayed_updating/unwind/nap.ma".
+include "delayed_updating/unwind/xap.ma".
 include "delayed_updating/syntax/path_head_depth.ma".
-include "delayed_updating/syntax/path_height.ma".
+include "ground/arith/nat_le_plus.ma".
 
 (* UNWIND MAP FOR PATH ******************************************************)
 
 (* Constructions with path_head *********************************************)
 
-lemma unwind2_rmap_head_push (f) (p) (n):
-      n + ♯(↳[n]p) = (▶[⫯f]↳[n]p)@↑❨n❩.
+lemma unwind2_rmap_head_xap_closed (f) (p) (n) (k):
+      (∃q. p = (↳[n]p)●q) → k ≤ n →
+      (▶[f]p)＠❨k❩ = (▶[f]↳[n]p)＠❨k❩.
+#f #p elim p -p
+[ #n #k * #q #Hq #Hk
+  elim (eq_inv_list_empty_append … Hq) -Hq * #_ //
+| #l #p #IH #n @(nat_ind_succ … n) -n
+  [ #k #_ #Hk <(nle_inv_zero_dx … Hk) -k -IH
+   <path_head_zero <unwind2_rmap_empty //
+  | #n #_ #k cases l [ #m ] * #q
+    [ <path_head_d_sn <list_append_lcons_sn #Hq #Hk
+      elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+      <unwind2_rmap_d_sn <unwind2_rmap_d_sn
+      <tr_compose_xap <tr_compose_xap
+      @IH [ /2 width=2 by ex_intro/ ] (**) (* auto too slow *)
+      @nle_trans [| @tr_uni_xap ]
+      /2 width=1 by nle_plus_bi_dx/
+    | <path_head_m_sn <list_append_lcons_sn #Hq #Hk
+      elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+      <unwind2_rmap_m_sn <unwind2_rmap_m_sn
+      /3 width=2 by ex_intro/
+    | <path_head_L_sn <list_append_lcons_sn #Hq
+      @(nat_ind_succ … k) -k // #k #_ #Hk
+      lapply (nle_inv_succ_bi … Hk) -Hk #Hk
+      elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+      <unwind2_rmap_L_sn <unwind2_rmap_L_sn
+      <tr_xap_push <tr_xap_push
+      /4 width=2 by ex_intro, eq_f/
+    | <path_head_A_sn <list_append_lcons_sn #Hq #Hk
+      elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+      <unwind2_rmap_A_sn <unwind2_rmap_A_sn
+      /3 width=2 by ex_intro/
+    | <path_head_S_sn <list_append_lcons_sn #Hq #Hk
+      elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
+      <unwind2_rmap_S_sn <unwind2_rmap_S_sn
+      /3 width=2 by ex_intro/
+    ]
+  ]
+]
+qed-.
+
+lemma unwind2_rmap_head_xap (f) (p) (n):
+      n + ♯(↳[n]p) = (▶[f]↳[n]p)＠❨n❩.
 #f #p elim p -p
 [ #n <path_head_empty <unwind2_rmap_labels_L <height_labels_L
-  >tr_pushs_swap <tr_nap_pushs_lt //
+  <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_nap //
+    <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_nap_push <npred_succ //
+    <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 //
   ]
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma
index 6eb8b3ae8..0ea3ab8ac 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma
@@ -25,7 +25,7 @@ match p with
   match l with
   [ label_d n ⇒
     match q with
-    [ list_empty     ⇒ 𝗱((f n)＠⧣❨n❩)◗(unwind_gen f q)
+    [ list_empty     ⇒ 𝗱(f＠⧣❨n❩)◗(unwind_gen f q)
     | list_lcons _ _ ⇒ unwind_gen f q
     ]
   | label_m   ⇒ unwind_gen f q
@@ -46,7 +46,7 @@ lemma unwind_gen_empty (f):
 // qed.
 
 lemma unwind_gen_d_empty (f) (n):
-      𝗱((f n)＠⧣❨n❩)◗𝐞 = ◆[f](𝗱n◗𝐞).
+      𝗱(f＠⧣❨n❩)◗𝐞 = ◆[f](𝗱n◗𝐞).
 // qed.
 
 lemma unwind_gen_d_lcons (f) (p) (l) (n):
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
index a9b2683b6..2954be831 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
@@ -20,7 +20,6 @@ include "ground/relocation/tr_compose_pap.ma".
 (* Properties with tr_compose ***********************************************)
 
 lemma unwind_gen_after (f2) (f1) (p):
-      ◆[f2]◆[f1]p = ◆[λn.(f2 ((f1 n)＠⧣❨n❩))∘(f1 n)]p.
+      ◆[f2]◆[f1]p = ◆[f2∘f1]p.
 #f2 #f1 #p @(path_ind_unwind … p) -p //
-#n #_ <unwind_gen_d_empty <unwind_gen_d_empty //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.ma
index 34cb91a5a..11ddd2d03 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.ma
@@ -19,15 +19,11 @@ include "ground/relocation/tr_pap_eq.ma".
 
 (* Constructions with stream_eq *********************************************)
 
-lemma unwind_gen_eq_repl (p) (f1) (f2):
-      (∀n. f1 n ≗ f2 n) → ◆[f1]p = ◆[f2]p.
-#p @(path_ind_unwind … p) -p // [ #n | #n #l #p |*: #p ] #IH #f1 #f2 #Hf
+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 n)) -f2 -IH //
-| <unwind_gen_d_lcons <unwind_gen_d_lcons
-  <(IH … Hf) -f2 -IH //
-| <unwind_gen_m_sn <unwind_gen_m_sn
-  <(IH … Hf) -f2 -IH //
+  <(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
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
index fcc04282b..d8a44810c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
@@ -73,29 +73,29 @@ qed-.
 
 (* Advanced constructions with list_rcons ***********************************)
 
-lemma unwind_gen_d_empty_dx (n) (p) (f):
-      (⊗p)◖𝗱((f n)＠⧣❨n❩) = ◆[f](p◖𝗱n).
-#n #p #f <unwind_gen_append_proper_dx // 
+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 (p) (f):
+lemma unwind_gen_m_dx (f) (p):
       ⊗p = ◆[f](p◖𝗺).
-#p #f <unwind_gen_append_proper_dx //
+#f #p <unwind_gen_append_proper_dx //
 qed.
 
-lemma unwind_gen_L_dx (p) (f):
+lemma unwind_gen_L_dx (f) (p):
       (⊗p)◖𝗟 = ◆[f](p◖𝗟).
-#p #f <unwind_gen_append_proper_dx //
+#f #p <unwind_gen_append_proper_dx //
 qed.
 
-lemma unwind_gen_A_dx (p) (f):
+lemma unwind_gen_A_dx (f) (p):
       (⊗p)◖𝗔 = ◆[f](p◖𝗔).
-#p #f <unwind_gen_append_proper_dx //
+#f #p <unwind_gen_append_proper_dx //
 qed.
 
-lemma unwind_gen_S_dx (p) (f):
+lemma unwind_gen_S_dx (f) (p):
       (⊗p)◖𝗦 = ◆[f](p◖𝗦).
-#p #f <unwind_gen_append_proper_dx //
+#f #p <unwind_gen_append_proper_dx //
 qed.
 
 lemma unwind_gen_root (f) (p):
@@ -110,7 +110,7 @@ qed-.
 
 lemma unwind_gen_inv_d_sn (k) (q) (p) (f):
       (𝗱k◗q) = ◆[f]p →
-      ∃∃r,h. 𝐞 = ⊗r & (f h)＠⧣❨h❩ = k & 𝐞 = q & r◖𝗱h = 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
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/xap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/xap.ma
new file mode 100644
index 000000000..f10ced5d6
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/xap.ma
@@ -0,0 +1,55 @@
+include "delayed_updating/unwind/nap.ma".
+include "ground/notation/functions/apply_2.ma".
+include "ground/relocation/tr_compose_pn.ma".
+
+definition tr_xap (f) (l:nat): nat ≝
+           (⫯f)@↑❨l❩.
+
+interpretation
+  "functional extended application (total relocation maps)"
+  'Apply f l = (tr_xap f l).
+
+lemma tr_xap_unfold (f) (l):
+      (⫯f)@↑❨l❩ = f＠❨l❩.
+// qed.
+
+lemma tr_xap_zero (f):
+      (𝟎) = f＠❨𝟎❩.
+// qed.
+
+lemma tr_xap_ninj (f) (p):
+      ninj (f＠⧣❨p❩) = f＠❨ninj p❩.
+// qed.
+
+lemma tr_compose_xap (f2) (f1) (l):
+      f2＠❨f1＠❨l❩❩ = (f2∘f1)＠❨l❩.
+#f2 #f1 #l
+<tr_xap_unfold <tr_xap_unfold <tr_xap_unfold
+>tr_compose_nap >tr_compose_push_bi //
+qed.
+
+lemma tr_uni_xap_succ (n) (m):
+      ↑m + n = 𝐮❨n❩＠❨↑m❩.
+#n #m
+<tr_xap_unfold
+<tr_nap_push <tr_uni_nap //
+qed.
+
+lemma tr_uni_xap (n) (m):
+      𝐮❨n❩＠❨m❩ ≤ m+n.
+#n #m @(nat_ind_succ … m) -m //
+qed.
+
+lemma tr_xap_push (f) (l):
+      ↑(f＠❨l❩) = (⫯f)＠❨↑l❩.
+#f #l
+<tr_xap_unfold <tr_xap_unfold
+<tr_nap_push //
+qed.
+
+lemma tr_xap_pushs_le (f) (n) (m):
+      m ≤ n → m = (⫯*[n]f)＠❨m❩.
+#f #n #m #Hmn
+<tr_xap_unfold >tr_pushs_succ <tr_nap_pushs_lt //
+/2 width=1 by nlt_succ_dx/
+qed-.
-- 
2.39.2