From dfcad1c1a698bac1b7fb6a5f59393b28f45182af Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 17 May 2022 17:51:39 +0200
Subject: [PATCH] update in delayed_updating

+ generic unwind for path
+ some old files parked
---
 .../black_downtriangle_4.etc}                 |   0
 .../etc/{unwind3 => lift1}/lift.etc           |  24 +-
 .../etc/{unwind3 => lift1}/lift_after.etc     |   9 +-
 .../{unwind3 => lift1}/lift_constructors.etc  |  20 +-
 .../etc/{unwind3 => lift1}/lift_eq.etc        |  57 +++-
 .../lift1/lift_length.etc}                    |   0
 .../etc/{unwind3 => lift1}/lift_prototerm.etc |   0
 .../{unwind3 => lift1}/lift_prototerm_eq.etc  |  17 ++
 .../lift1/lift_structure.etc}                 |   0
 .../etc/{unwind3 => lift1}/lift_uni.etc       |   8 +-
 .../unwind0/unwind1_path.etc}                 |   0
 .../unwind0/unwind1_path_structure.etc}       |   0
 .../unwind0/unwind1_rmap.etc}                 |   0
 .../unwind0/unwind1_rmap_eq.etc}              |   0
 .../unwind0/unwind2_path.etc}                 |   0
 .../unwind0/unwind2_path_structure.etc}       |   0
 .../unwind0/unwind2_rmap.etc}                 |   0
 .../unwind0/unwind2_rmap_eq.etc}              |   0
 .../notation/functions/black_diamond_2.ma     |  19 ++
 .../delayed_updating/substitution/lift.ma     |  24 +-
 .../substitution/lift_after.ma                |   9 +-
 .../substitution/lift_constructors.ma         |  20 +-
 .../delayed_updating/substitution/lift_eq.ma  |  57 +---
 .../lift_id.etc => substitution/lift_id.ma}   |   0
 .../substitution/lift_prototerm_eq.ma         |  17 --
 .../lift_prototerm_id.ma}                     |   0
 .../delayed_updating/substitution/lift_uni.ma |   8 +-
 .../syntax/path_depth_labels.ma               |  26 ++
 .../syntax/{path_tail.ma => path_head.ma}     |  32 +--
 ...{path_tail_depth.ma => path_head_depth.ma} |  31 +-
 .../syntax/path_height_labels.ma              |  26 ++
 .../delayed_updating/unwind/nap.ma            |  52 ++++
 .../delayed_updating/unwind/unwind1_rmap.ma   |  63 ----
 .../unwind/unwind1_rmap_tail.ma               |  82 ------
 .../delayed_updating/unwind/unwind2_rmap.ma   | 103 +++++++
 .../unwind/unwind2_rmap_eq.ma                 |  33 +++
 .../unwind/unwind2_rmap_head.ma               |  40 +++
 .../unwind/unwind2_rmap_labels.ma             |  28 ++
 .../unwind/unwind2_rmap_structure.ma          |  31 ++
 .../delayed_updating/unwind/unwind_gen.ma     |  86 ++++++
 .../unwind/unwind_gen_after.ma                |  25 ++
 .../delayed_updating/unwind/unwind_gen_eq.ma  |  34 +++
 .../unwind/unwind_gen_structure.ma            | 269 ++++++++++++++++++
 matita/matita/predefined_virtuals.ml          |   2 +-
 44 files changed, 935 insertions(+), 317 deletions(-)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{notation/functions/black_downtriangle_4.ma => etc/black_downtriangle_4.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/etc/{unwind3 => lift1}/lift.etc (89%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/etc/{unwind3 => lift1}/lift_after.etc (86%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/etc/{unwind3 => lift1}/lift_constructors.etc (77%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/etc/{unwind3 => lift1}/lift_eq.etc (77%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{substitution/lift_length.ma => etc/lift1/lift_length.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/etc/{unwind3 => lift1}/lift_prototerm.etc (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/etc/{unwind3 => lift1}/lift_prototerm_eq.etc (85%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{substitution/lift_structure.ma => etc/lift1/lift_structure.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/etc/{unwind3 => lift1}/lift_uni.etc (88%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind0/unwind1_path.ma => etc/unwind0/unwind1_path.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind0/unwind1_path_structure.ma => etc/unwind0/unwind1_path_structure.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind0/unwind1_rmap.ma => etc/unwind0/unwind1_rmap.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind0/unwind1_rmap_eq.ma => etc/unwind0/unwind1_rmap_eq.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind0/unwind2_path.ma => etc/unwind0/unwind2_path.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind0/unwind2_path_structure.ma => etc/unwind0/unwind2_path_structure.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind0/unwind2_rmap.ma => etc/unwind0/unwind2_rmap.etc} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{unwind0/unwind2_rmap_eq.ma => etc/unwind0/unwind2_rmap_eq.etc} (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_diamond_2.ma
 rename matita/matita/contribs/lambdadelta/delayed_updating/{etc/unwind3/lift_id.etc => substitution/lift_id.ma} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/{etc/unwind3/lift_prototerm_id.etc => substitution/lift_prototerm_id.ma} (100%)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth_labels.ma
 rename matita/matita/contribs/lambdadelta/delayed_updating/syntax/{path_tail.ma => path_head.ma} (75%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/syntax/{path_tail_depth.ma => path_head_depth.ma} (66%)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height_labels.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/nap.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind1_rmap.ma
 delete mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind1_rmap_tail.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_labels.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_structure.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.ma
 create 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_downtriangle_4.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/black_downtriangle_4.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_downtriangle_4.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/black_downtriangle_4.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift.etc
similarity index 89%
rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift.etc
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift.etc
index a487fcf5a..e6e1e661e 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift.etc
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift.etc
@@ -15,8 +15,7 @@
 include "delayed_updating/notation/functions/uparrow_4.ma".
 include "delayed_updating/notation/functions/uparrow_2.ma".
 include "delayed_updating/syntax/path.ma".
-include "ground/relocation/tr_uni.ma".
-include "ground/relocation/tr_pap_tls.ma".
+include "ground/relocation/tr_id_pap.ma".
 
 (* LIFT FOR PATH ***********************************************************)
 
@@ -28,7 +27,7 @@ match p with
 [ list_empty     ⇒ k f (𝐞)
 | list_lcons l q ⇒
   match l with
-  [ label_d n ⇒ lift_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (⇂*[n]f) q
+  [ label_d n ⇒ lift_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (𝐢) q
   | label_m   ⇒ lift_gen (A) (λg,p. k g (𝗺◗p)) f q
   | label_L   ⇒ lift_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q
   | label_A   ⇒ lift_gen (A) (λg,p. k g (𝗔◗p)) f q
@@ -61,7 +60,7 @@ lemma lift_empty (A) (k) (f):
 // qed.
 
 lemma lift_d_sn (A) (k) (p) (n) (f):
-      ↑❨(λg,p. k g (𝗱(f@❨n❩)◗p)), ⇂*[n]f, p❩ = ↑{A}❨k, f, 𝗱n◗p❩.
+      ↑❨(λg,p. k g (𝗱(f@❨n❩)◗p)), 𝐢, p❩ = ↑{A}❨k, f, 𝗱n◗p❩.
 // qed.
 
 lemma lift_m_sn (A) (k) (p) (f):
@@ -93,7 +92,7 @@ lemma lift_rmap_empty (f):
 // qed.
 
 lemma lift_rmap_d_sn (f) (p) (n):
-      ↑[p](⇂*[ninj n]f) = ↑[𝗱n◗p]f.
+      ↑[p]𝐢 = ↑[𝗱n◗p]f.
 // qed.
 
 lemma lift_rmap_m_sn (f) (p):
@@ -112,12 +111,21 @@ lemma lift_rmap_S_sn (f) (p):
       ↑[p]f = ↑[𝗦◗p]f.
 // qed.
 
+(* Advanced cinstructionswith proj_rmap and tr_id ***************************)
+
+lemma lift_rmap_id (p):
+      (𝐢) = ↑[p]𝐢.
+#p elim p -p //
+* [ #n ] #p #IH //
+qed.
+
 (* Advanced constructions with proj_rmap and path_append ********************)
 
 lemma lift_rmap_append (p2) (p1) (f):
       ↑[p2]↑[p1]f = ↑[p1●p2]f.
 #p2 #p1 elim p1 -p1 // * [ #n ] #p1 #IH #f //
-[ <lift_rmap_m_sn <lift_rmap_m_sn //
+[ <lift_rmap_d_sn <lift_rmap_d_sn //
+| <lift_rmap_m_sn <lift_rmap_m_sn //
 | <lift_rmap_A_sn <lift_rmap_A_sn //
 | <lift_rmap_S_sn <lift_rmap_S_sn //
 ]
@@ -126,7 +134,7 @@ qed.
 (* Advanced constructions with proj_rmap and path_rcons *********************)
 
 lemma lift_rmap_d_dx (f) (p) (n):
-      ⇂*[ninj n](↑[p]f) = ↑[p◖𝗱n]f.
+      (𝐢) = ↑[p◖𝗱n]f.
 // qed.
 
 lemma lift_rmap_m_dx (f) (p):
@@ -146,5 +154,5 @@ lemma lift_rmap_S_dx (f) (p):
 // qed.
 
 lemma lift_rmap_pap_d_dx (f) (p) (n) (m):
-      ↑[p]f@❨m+n❩ = ↑[p◖𝗱n]f@❨m❩+↑[p]f@❨n❩.
+      m = ↑[p◖𝗱n]f@❨m❩.
 // qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_after.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_after.etc
similarity index 86%
rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_after.etc
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_after.etc
index 756b73587..02b2c6ee1 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_after.etc
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_after.etc
@@ -15,7 +15,6 @@
 include "delayed_updating/substitution/lift_eq.ma".
 include "ground/relocation/tr_compose_pap.ma".
 include "ground/relocation/tr_compose_pn.ma".
-include "ground/relocation/tr_compose_tls.ma".
 
 (* LIFT FOR PATH ***********************************************************)
 
@@ -23,9 +22,7 @@ include "ground/relocation/tr_compose_tls.ma".
 
 lemma lift_path_after (p) (f1) (f2):
       ↑[f2]↑[f1]p = ↑[f2∘f1]p.
-#p elim p -p [| * ] // [ #n ] #p #IH #f1 #f2
-[ <lift_path_d_sn <lift_path_d_sn <lift_path_d_sn //
-| <lift_path_L_sn <lift_path_L_sn <lift_path_L_sn
-  >tr_compose_push_bi //
-]
+#p elim p -p [| * ] // #p #IH #f1 #f2
+<lift_path_L_sn <lift_path_L_sn <lift_path_L_sn
+>tr_compose_push_bi //
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_constructors.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_constructors.etc
similarity index 77%
rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_constructors.etc
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_constructors.etc
index 772c837fb..3bd7b43bc 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_constructors.etc
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_constructors.etc
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/substitution/lift_prototerm_id.ma".
+include "delayed_updating/substitution/lift_prototerm_eq.ma".
 include "delayed_updating/substitution/lift_uni.ma".
 include "delayed_updating/syntax/prototerm_constructors.ma".
 
@@ -24,28 +24,24 @@ lemma lift_iref_bi (t1) (t2) (n):
 qed.
 
 lemma lift_iref_sn (f) (t:prototerm) (n:pnat):
-      (𝛗f@❨n❩.↑[⇂*[n]f]t) ⊆ ↑[f](𝛗n.t).
-#f #t #n #p * #q * #r #Hr #H1 #H2 destruct
-@(ex2_intro … (𝗱n◗𝗺◗r))
+      (𝛗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 lift_iref_dx (f) (t) (n:pnat):
-      ↑[f](𝛗n.t) ⊆ 𝛗f@❨n❩.↑[⇂*[n]f]t.
+      ↑[f](𝛗n.t) ⊆ 𝛗f@❨n❩.t.
 #f #t #n #p * #q #Hq #H0 destruct
 elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct
-/3 width=1 by in_comp_iref, in_comp_lift_bi/
+/2 width=1 by in_comp_iref/
 qed-.
 
 lemma lift_iref (f) (t) (n:pnat):
-      (𝛗f@❨n❩.↑[⇂*[n]f]t) ⇔ ↑[f](𝛗n.t).
+      (𝛗f@❨n❩.t) ⇔ ↑[f](𝛗n.t).
 /3 width=1 by conj, lift_iref_sn, lift_iref_dx/
 qed.
 
 lemma lift_iref_uni (t) (m) (n):
       (𝛗(n+m).t) ⇔ ↑[𝐮❨m❩](𝛗n.t).
-#t #m #n
-@(subset_eq_trans … (lift_iref …))
-<tr_uni_pap >nsucc_pnpred <tr_tls_succ_uni
-/3 width=1 by lift_iref_bi, lift_term_id/
-qed.
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_eq.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_eq.etc
similarity index 77%
rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_eq.etc
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_eq.etc
index fad4995de..1e9b2789b 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_eq.etc
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_eq.etc
@@ -13,14 +13,8 @@
 (**************************************************************************)
 
 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".
 
 (* LIFT FOR PATH ***********************************************************)
 
@@ -39,7 +33,7 @@ lemma lift_eq_repl (A) (p) (k1) (k2):
 #k1 #k2 #Hk #f1 #f2 #Hf
 [ <lift_empty <lift_empty /2 width=1 by/
 | <lift_d_sn <lift_d_sn <(tr_pap_eq_repl … Hf)
-  /3 width=3 by stream_tls_eq_repl, compose_repl_fwd_sn/
+  /3 width=1 by stream_eq_refl/
 | /3 width=1 by/
 | /3 width=1 by tr_push_eq_repl/
 | /3 width=1 by/
@@ -92,7 +86,7 @@ lemma lift_path_lcons (f) (p) (l):
 qed.
 
 lemma lift_path_d_sn (f) (p) (n):
-      (𝗱(f@❨n❩)◗↑[⇂*[n]f]p) = ↑[f](𝗱n◗p).
+      (𝗱(f@❨n❩)◗↑[𝐢]p) = ↑[f](𝗱n◗p).
 // qed.
 
 lemma lift_path_m_sn (f) (p):
@@ -110,6 +104,53 @@ lemma lift_path_A_sn (f) (p):
 lemma lift_path_S_sn (f) (p):
       (𝗦◗↑[f]p) = ↑[f](𝗦◗p).
 // qed.
+
+lemma lift_path_id (p):
+      p = ↑[𝐢]p.
+#p elim p -p //
+* [ #n ] #p #IH //
+[ <lift_path_d_sn //
+| <lift_path_L_sn //
+]
+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 (n) (p) (f):
+      (↑[f]p)◖𝗱((↑[p]f)@❨n❩) = ↑[f](p◖𝗱n).
+#n #p #f <lift_path_append //
+qed.
+
+lemma lift_path_m_dx (p) (f):
+      (↑[f]p)◖𝗺 = ↑[f](p◖𝗺).
+#p #f <lift_path_append //
+qed.
+
+lemma lift_path_L_dx (p) (f):
+      (↑[f]p)◖𝗟 = ↑[f](p◖𝗟).
+#p #f <lift_path_append //
+qed.
+
+lemma lift_path_A_dx (p) (f):
+      (↑[f]p)◖𝗔 = ↑[f](p◖𝗔).
+#p #f <lift_path_append //
+qed.
+
+lemma lift_path_S_dx (p) (f):
+      (↑[f]p)◖𝗦 = ↑[f](p◖𝗦).
+#p #f <lift_path_append //
+qed.
+
 (* COMMENT 
 
 (* Advanced constructions with proj_rmap and stream_tls *********************)
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_length.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_length.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_length.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_length.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_prototerm.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_prototerm.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_prototerm.etc
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_prototerm.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_prototerm_eq.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_prototerm_eq.etc
similarity index 85%
rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_prototerm_eq.etc
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_prototerm_eq.etc
index fc3fb3fcf..55b271f8b 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_prototerm_eq.etc
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_prototerm_eq.etc
@@ -38,3 +38,20 @@ lemma lift_term_after (f1) (f2) (t):
 | @subset_equivalence_ext_f1_exteq /2 width=5/
 ]
 qed.
+
+lemma lift_term_id_sn (t):
+      t ⊆ ↑[𝐢]t.
+#t #p #Hp
+>(lift_path_id p)
+/2 width=1 by in_comp_lift_bi/
+qed-.
+
+lemma lift_term_id_dx (t):
+      ↑[𝐢]t ⊆ t.
+#t #p * #q #Hq #H destruct //
+qed-.
+
+lemma lift_term_id (t):
+      t ⇔ ↑[𝐢]t.
+/3 width=2 by lift_term_id_dx, lift_term_id_sn, conj/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_structure.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_structure.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_uni.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_uni.etc
similarity index 88%
rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_uni.etc
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_uni.etc
index cd6c79533..c0b04d975 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_uni.etc
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift1/lift_uni.etc
@@ -12,9 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/substitution/lift_id.ma".
+include "delayed_updating/substitution/lift_eq.ma".
 include "ground/relocation/tr_uni_pap.ma".
-include "ground/relocation/tr_uni_tls.ma".
 
 (* LIFT FOR PATH ***********************************************************)
 
@@ -22,7 +21,4 @@ include "ground/relocation/tr_uni_tls.ma".
 
 lemma lift_path_d_sn_uni (p) (m) (n):
       (𝗱(n+m)◗p) = ↑[𝐮❨m❩](𝗱(n)◗p).
-#p #m #n
-<lift_path_d_sn <tr_uni_pap >nsucc_pnpred
-<tr_tls_succ_uni //
-qed.
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_path.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind1_path.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_path.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind1_path.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind1_path_structure.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_path_structure.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind1_path_structure.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind1_rmap.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_rmap.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind1_rmap.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind1_rmap_eq.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_rmap_eq.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind1_rmap_eq.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_path.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind2_path.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_path.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind2_path.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind2_path_structure.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_path_structure.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind2_path_structure.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind2_rmap.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_rmap.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind2_rmap.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_rmap_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind2_rmap_eq.etc
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_rmap_eq.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind0/unwind2_rmap_eq.etc
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_diamond_2.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_diamond_2.ma
new file mode 100644
index 000000000..8aff1451a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/black_diamond_2.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( ◆[ term 46 f ] break term 70 p )"
+  non associative with precedence 70
+  for @{ 'BlackDiamond $f $p }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
index e6e1e661e..a487fcf5a 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
@@ -15,7 +15,8 @@
 include "delayed_updating/notation/functions/uparrow_4.ma".
 include "delayed_updating/notation/functions/uparrow_2.ma".
 include "delayed_updating/syntax/path.ma".
-include "ground/relocation/tr_id_pap.ma".
+include "ground/relocation/tr_uni.ma".
+include "ground/relocation/tr_pap_tls.ma".
 
 (* LIFT FOR PATH ***********************************************************)
 
@@ -27,7 +28,7 @@ match p with
 [ list_empty     ⇒ k f (𝐞)
 | list_lcons l q ⇒
   match l with
-  [ label_d n ⇒ lift_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (𝐢) q
+  [ label_d n ⇒ lift_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (⇂*[n]f) q
   | label_m   ⇒ lift_gen (A) (λg,p. k g (𝗺◗p)) f q
   | label_L   ⇒ lift_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q
   | label_A   ⇒ lift_gen (A) (λg,p. k g (𝗔◗p)) f q
@@ -60,7 +61,7 @@ lemma lift_empty (A) (k) (f):
 // qed.
 
 lemma lift_d_sn (A) (k) (p) (n) (f):
-      ↑❨(λg,p. k g (𝗱(f@❨n❩)◗p)), 𝐢, p❩ = ↑{A}❨k, f, 𝗱n◗p❩.
+      ↑❨(λg,p. k g (𝗱(f@❨n❩)◗p)), ⇂*[n]f, p❩ = ↑{A}❨k, f, 𝗱n◗p❩.
 // qed.
 
 lemma lift_m_sn (A) (k) (p) (f):
@@ -92,7 +93,7 @@ lemma lift_rmap_empty (f):
 // qed.
 
 lemma lift_rmap_d_sn (f) (p) (n):
-      ↑[p]𝐢 = ↑[𝗱n◗p]f.
+      ↑[p](⇂*[ninj n]f) = ↑[𝗱n◗p]f.
 // qed.
 
 lemma lift_rmap_m_sn (f) (p):
@@ -111,21 +112,12 @@ lemma lift_rmap_S_sn (f) (p):
       ↑[p]f = ↑[𝗦◗p]f.
 // qed.
 
-(* Advanced cinstructionswith proj_rmap and tr_id ***************************)
-
-lemma lift_rmap_id (p):
-      (𝐢) = ↑[p]𝐢.
-#p elim p -p //
-* [ #n ] #p #IH //
-qed.
-
 (* Advanced constructions with proj_rmap and path_append ********************)
 
 lemma lift_rmap_append (p2) (p1) (f):
       ↑[p2]↑[p1]f = ↑[p1●p2]f.
 #p2 #p1 elim p1 -p1 // * [ #n ] #p1 #IH #f //
-[ <lift_rmap_d_sn <lift_rmap_d_sn //
-| <lift_rmap_m_sn <lift_rmap_m_sn //
+[ <lift_rmap_m_sn <lift_rmap_m_sn //
 | <lift_rmap_A_sn <lift_rmap_A_sn //
 | <lift_rmap_S_sn <lift_rmap_S_sn //
 ]
@@ -134,7 +126,7 @@ qed.
 (* Advanced constructions with proj_rmap and path_rcons *********************)
 
 lemma lift_rmap_d_dx (f) (p) (n):
-      (𝐢) = ↑[p◖𝗱n]f.
+      ⇂*[ninj n](↑[p]f) = ↑[p◖𝗱n]f.
 // qed.
 
 lemma lift_rmap_m_dx (f) (p):
@@ -154,5 +146,5 @@ lemma lift_rmap_S_dx (f) (p):
 // qed.
 
 lemma lift_rmap_pap_d_dx (f) (p) (n) (m):
-      m = ↑[p◖𝗱n]f@❨m❩.
+      ↑[p]f@❨m+n❩ = ↑[p◖𝗱n]f@❨m❩+↑[p]f@❨n❩.
 // qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_after.ma
index 02b2c6ee1..756b73587 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_after.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_after.ma
@@ -15,6 +15,7 @@
 include "delayed_updating/substitution/lift_eq.ma".
 include "ground/relocation/tr_compose_pap.ma".
 include "ground/relocation/tr_compose_pn.ma".
+include "ground/relocation/tr_compose_tls.ma".
 
 (* LIFT FOR PATH ***********************************************************)
 
@@ -22,7 +23,9 @@ include "ground/relocation/tr_compose_pn.ma".
 
 lemma lift_path_after (p) (f1) (f2):
       ↑[f2]↑[f1]p = ↑[f2∘f1]p.
-#p elim p -p [| * ] // #p #IH #f1 #f2
-<lift_path_L_sn <lift_path_L_sn <lift_path_L_sn
->tr_compose_push_bi //
+#p elim p -p [| * ] // [ #n ] #p #IH #f1 #f2
+[ <lift_path_d_sn <lift_path_d_sn <lift_path_d_sn //
+| <lift_path_L_sn <lift_path_L_sn <lift_path_L_sn
+  >tr_compose_push_bi //
+]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
index 3bd7b43bc..772c837fb 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_constructors.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/substitution/lift_prototerm_eq.ma".
+include "delayed_updating/substitution/lift_prototerm_id.ma".
 include "delayed_updating/substitution/lift_uni.ma".
 include "delayed_updating/syntax/prototerm_constructors.ma".
 
@@ -24,24 +24,28 @@ lemma lift_iref_bi (t1) (t2) (n):
 qed.
 
 lemma lift_iref_sn (f) (t:prototerm) (n:pnat):
-      (𝛗f@❨n❩.t) ⊆ ↑[f](𝛗n.t).
-#f #t #n #p * #q #Hq #H0 destruct
-@(ex2_intro … (𝗱n◗𝗺◗q))
+      (𝛗f@❨n❩.↑[⇂*[n]f]t) ⊆ ↑[f](𝛗n.t).
+#f #t #n #p * #q * #r #Hr #H1 #H2 destruct
+@(ex2_intro … (𝗱n◗𝗺◗r))
 /2 width=1 by in_comp_iref/
 qed-.
 
 lemma lift_iref_dx (f) (t) (n:pnat):
-      ↑[f](𝛗n.t) ⊆ 𝛗f@❨n❩.t.
+      ↑[f](𝛗n.t) ⊆ 𝛗f@❨n❩.↑[⇂*[n]f]t.
 #f #t #n #p * #q #Hq #H0 destruct
 elim (in_comp_inv_iref … Hq) -Hq #p #H0 #Hp destruct
-/2 width=1 by in_comp_iref/
+/3 width=1 by in_comp_iref, in_comp_lift_bi/
 qed-.
 
 lemma lift_iref (f) (t) (n:pnat):
-      (𝛗f@❨n❩.t) ⇔ ↑[f](𝛗n.t).
+      (𝛗f@❨n❩.↑[⇂*[n]f]t) ⇔ ↑[f](𝛗n.t).
 /3 width=1 by conj, lift_iref_sn, lift_iref_dx/
 qed.
 
 lemma lift_iref_uni (t) (m) (n):
       (𝛗(n+m).t) ⇔ ↑[𝐮❨m❩](𝛗n.t).
-// qed.
+#t #m #n
+@(subset_eq_trans … (lift_iref …))
+<tr_uni_pap >nsucc_pnpred <tr_tls_succ_uni
+/3 width=1 by lift_iref_bi, lift_term_id/
+qed.
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 1e9b2789b..fad4995de 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
@@ -13,8 +13,14 @@
 (**************************************************************************)
 
 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".
 
 (* LIFT FOR PATH ***********************************************************)
 
@@ -33,7 +39,7 @@ lemma lift_eq_repl (A) (p) (k1) (k2):
 #k1 #k2 #Hk #f1 #f2 #Hf
 [ <lift_empty <lift_empty /2 width=1 by/
 | <lift_d_sn <lift_d_sn <(tr_pap_eq_repl … Hf)
-  /3 width=1 by stream_eq_refl/
+  /3 width=3 by stream_tls_eq_repl, compose_repl_fwd_sn/
 | /3 width=1 by/
 | /3 width=1 by tr_push_eq_repl/
 | /3 width=1 by/
@@ -86,7 +92,7 @@ lemma lift_path_lcons (f) (p) (l):
 qed.
 
 lemma lift_path_d_sn (f) (p) (n):
-      (𝗱(f@❨n❩)◗↑[𝐢]p) = ↑[f](𝗱n◗p).
+      (𝗱(f@❨n❩)◗↑[⇂*[n]f]p) = ↑[f](𝗱n◗p).
 // qed.
 
 lemma lift_path_m_sn (f) (p):
@@ -104,53 +110,6 @@ lemma lift_path_A_sn (f) (p):
 lemma lift_path_S_sn (f) (p):
       (𝗦◗↑[f]p) = ↑[f](𝗦◗p).
 // qed.
-
-lemma lift_path_id (p):
-      p = ↑[𝐢]p.
-#p elim p -p //
-* [ #n ] #p #IH //
-[ <lift_path_d_sn //
-| <lift_path_L_sn //
-]
-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 (n) (p) (f):
-      (↑[f]p)◖𝗱((↑[p]f)@❨n❩) = ↑[f](p◖𝗱n).
-#n #p #f <lift_path_append //
-qed.
-
-lemma lift_path_m_dx (p) (f):
-      (↑[f]p)◖𝗺 = ↑[f](p◖𝗺).
-#p #f <lift_path_append //
-qed.
-
-lemma lift_path_L_dx (p) (f):
-      (↑[f]p)◖𝗟 = ↑[f](p◖𝗟).
-#p #f <lift_path_append //
-qed.
-
-lemma lift_path_A_dx (p) (f):
-      (↑[f]p)◖𝗔 = ↑[f](p◖𝗔).
-#p #f <lift_path_append //
-qed.
-
-lemma lift_path_S_dx (p) (f):
-      (↑[f]p)◖𝗦 = ↑[f](p◖𝗦).
-#p #f <lift_path_append //
-qed.
-
 (* COMMENT 
 
 (* Advanced constructions with proj_rmap and stream_tls *********************)
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_id.etc b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_id.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_id.etc
rename to matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_id.ma
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma
index 55b271f8b..fc3fb3fcf 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_eq.ma
@@ -38,20 +38,3 @@ lemma lift_term_after (f1) (f2) (t):
 | @subset_equivalence_ext_f1_exteq /2 width=5/
 ]
 qed.
-
-lemma lift_term_id_sn (t):
-      t ⊆ ↑[𝐢]t.
-#t #p #Hp
->(lift_path_id p)
-/2 width=1 by in_comp_lift_bi/
-qed-.
-
-lemma lift_term_id_dx (t):
-      ↑[𝐢]t ⊆ t.
-#t #p * #q #Hq #H destruct //
-qed-.
-
-lemma lift_term_id (t):
-      t ⇔ ↑[𝐢]t.
-/3 width=2 by lift_term_id_dx, lift_term_id_sn, conj/
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_prototerm_id.etc b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_id.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/lift_prototerm_id.etc
rename to matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_id.ma
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_uni.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_uni.ma
index c0b04d975..cd6c79533 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_uni.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_uni.ma
@@ -12,8 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/substitution/lift_eq.ma".
+include "delayed_updating/substitution/lift_id.ma".
 include "ground/relocation/tr_uni_pap.ma".
+include "ground/relocation/tr_uni_tls.ma".
 
 (* LIFT FOR PATH ***********************************************************)
 
@@ -21,4 +22,7 @@ include "ground/relocation/tr_uni_pap.ma".
 
 lemma lift_path_d_sn_uni (p) (m) (n):
       (𝗱(n+m)◗p) = ↑[𝐮❨m❩](𝗱(n)◗p).
-// qed.
+#p #m #n
+<lift_path_d_sn <tr_uni_pap >nsucc_pnpred
+<tr_tls_succ_uni //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth_labels.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth_labels.ma
new file mode 100644
index 000000000..1993633de
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_depth_labels.ma
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_depth.ma".
+include "delayed_updating/syntax/path_labels.ma".
+
+(* DEPTH FOR PATH ***********************************************************)
+
+(* Constructions with labels ************************************************)
+
+lemma depth_labels_L (n):
+      n = ♭(𝗟∗∗n).
+#n @(nat_ind_succ … n) -n //
+#n #IH <labels_succ <depth_L_sn //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_tail.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head.ma
similarity index 75%
rename from matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_tail.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head.ma
index 193cc68e4..827af4489 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_tail.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head.ma
@@ -17,9 +17,9 @@ include "delayed_updating/notation/functions/downarrowright_2.ma".
 include "ground/arith/nat_plus.ma".
 include "ground/arith/nat_pred_succ.ma".
 
-(* TAIL FOR PATH ************************************************************)
+(* HEAD FOR PATH ************************************************************)
 
-rec definition tail (m) (p) on p: path ≝
+rec definition path_head (m) (p) on p: path ≝
 match m with
 [ nzero  ⇒ 𝐞
 | ninj o ⇒ 
@@ -27,47 +27,47 @@ match m with
   [ list_empty     ⇒ 𝗟∗∗m
   | list_lcons l q ⇒
     match l with
-    [ label_d n ⇒ l◗(tail (m+n) q)
-    | label_m   ⇒ l◗(tail m q)
-    | label_L   ⇒ l◗(tail (↓o) q)
-    | label_A   ⇒ l◗(tail m q)
-    | label_S   ⇒ l◗(tail m q)
+    [ label_d n ⇒ l◗(path_head (m+n) q)
+    | label_m   ⇒ l◗(path_head m q)
+    | label_L   ⇒ l◗(path_head (↓o) q)
+    | label_A   ⇒ l◗(path_head m q)
+    | label_S   ⇒ l◗(path_head m q)
     ]
   ]
 ].
 
 interpretation
-  "tail (reversed path)"
-  'DownArrowRight n p = (tail n p).
+  "head (reversed path)"
+  'DownArrowRight n p = (path_head n p).
 
 (* basic constructions ****************************************************)
 
-lemma tail_zero (p):
+lemma path_head_zero (p):
       (𝐞) = ↳[𝟎]p.
 * // qed.
 
-lemma tail_empty (n):
+lemma path_head_empty (n):
       (𝗟∗∗n) = ↳[n]𝐞.
 * // qed.
 
-lemma tail_d_sn (p) (n) (m:pnat):
+lemma path_head_d_sn (p) (n) (m:pnat):
       (𝗱m◗↳[↑n+m]p) = ↳[↑n](𝗱m◗p).
 // qed.
 
-lemma tail_m_sn (p) (n):
+lemma path_head_m_sn (p) (n):
       (𝗺◗↳[↑n]p) = ↳[↑n](𝗺◗p).
 // qed.
 
-lemma tail_L_sn (p) (n):
+lemma path_head_L_sn (p) (n):
       (𝗟◗↳[n]p) = ↳[↑n](𝗟◗p).
 #p #n
 whd in ⊢ (???%); //
 qed.
 
-lemma tail_A_sn (p) (n):
+lemma path_head_A_sn (p) (n):
       (𝗔◗↳[↑n]p) = ↳[↑n](𝗔◗p).
 // qed.
 
-lemma tail_S_sn (p) (n):
+lemma path_head_S_sn (p) (n):
       (𝗦◗↳[↑n]p) = ↳[↑n](𝗦◗p).
 // qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_tail_depth.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_depth.ma
similarity index 66%
rename from matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_tail_depth.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_depth.ma
index bccbea075..32138ee12 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_tail_depth.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_head_depth.ma
@@ -12,33 +12,24 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/syntax/path_tail.ma".
-include "delayed_updating/syntax/path_depth.ma".
-include "delayed_updating/syntax/path_height.ma".
-(*
-include "ground/arith/nat_plus.ma".
-include "ground/arith/nat_pred_succ.ma".
-*)
-(* TAIL FOR PATH ************************************************************)
+include "delayed_updating/syntax/path_head.ma".
+include "delayed_updating/syntax/path_depth_labels.ma".
+include "delayed_updating/syntax/path_height_labels.ma".
 
-(* Constructions with depth and height **************************************)
-
-axiom depth_lablels_L (n):
-      n = ♭(𝗟∗∗n).
+(* HEAD FOR PATH ************************************************************)
 
-axiom height_lablels_L (n):
-      (𝟎) = ♯(𝗟∗∗n).
+(* Constructions with depth and height **************************************)
 
-lemma tail_depth (p) (n):
+lemma path_head_depth (p) (n):
       n + ♯(↳[n]p) = ♭↳[n]p.
 #p elim p -p // #l #p #IH
 #n @(nat_ind_succ … n) -n // #n #_
 cases l [ #m ]
-[ <tail_d_sn <height_d_sn <depth_d_sn //
-| <tail_m_sn <height_m_sn <depth_m_sn //
-| <tail_L_sn <height_L_sn <depth_L_sn
+[ <path_head_d_sn <height_d_sn <depth_d_sn //
+| <path_head_m_sn <height_m_sn <depth_m_sn //
+| <path_head_L_sn <height_L_sn <depth_L_sn
   <nplus_succ_sn //
-| <tail_A_sn <height_A_sn <depth_A_sn //
-| <tail_S_sn <height_S_sn <depth_S_sn //
+| <path_head_A_sn <height_A_sn <depth_A_sn //
+| <path_head_S_sn <height_S_sn <depth_S_sn //
 ]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height_labels.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height_labels.ma
new file mode 100644
index 000000000..cf9a6d5c2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path_height_labels.ma
@@ -0,0 +1,26 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_height.ma".
+include "delayed_updating/syntax/path_labels.ma".
+
+(* HEIGHT FOR PATH **********************************************************)
+
+(* Constructions with labels ************************************************)
+
+lemma height_labels_L (n):
+      (𝟎) = ♯(𝗟∗∗n).
+#n @(nat_ind_succ … n) -n //
+#n #IH <labels_succ <height_L_sn //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/nap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/nap.ma
new file mode 100644
index 000000000..502765a0a
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/nap.ma
@@ -0,0 +1,52 @@
+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".
+include "ground/arith/nat_pred_succ.ma".
+
+lemma nlt_npsucc_bi (n1) (n2):
+      n1 < n2 → npsucc n1 < npsucc n2.
+#n1 #n2 #Hn elim Hn -n2 //
+#n2 #_ #IH /2 width=1 by plt_succ_dx_trans/
+qed.
+
+definition tr_nap (f) (l:nat): nat ≝
+           ↓(f@❨↑l❩).
+
+interpretation
+  "functional non-negative application (total relocation maps)"
+  'ApplySucc f l = (tr_nap f l).
+
+lemma tr_nap_unfold (f) (l):
+      ↓(f@❨↑l❩) = f@↑❨l❩.
+// qed.
+
+lemma tr_compose_nap (f2) (f1) (l):
+      f2@↑❨f1@↑❨l❩❩ = (f2∘f1)@↑❨l❩.
+#f2 #f1 #l
+<tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
+<tr_compose_pap <npsucc_pred //
+qed.
+
+lemma tr_uni_nap (n) (m):
+      m + n = 𝐮❨n❩@↑❨m❩.
+#n #m
+<tr_nap_unfold
+<tr_uni_pap <nrplus_npsucc_sn //
+qed.
+
+lemma tr_nap_push (f):
+      ∀l. ↑(f@↑❨l❩) = (⫯f)@↑❨↑l❩.
+#f #l
+<tr_nap_unfold <tr_nap_unfold
+<tr_pap_push <pnpred_psucc //
+qed.
+
+lemma tr_nap_pushs_lt (f) (n) (m):
+      m < n → m = (⫯*[n]f)@↑❨m❩.
+#f #n #m #Hmn
+<tr_nap_unfold <tr_pap_pushs_le
+/2 width=1 by nlt_npsucc_bi/
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind1_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind1_rmap.ma
deleted file mode 100644
index b94f56d5a..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind1_rmap.ma
+++ /dev/null
@@ -1,63 +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_righttriangle_1.ma".
-include "ground/relocation/tr_uni.ma".
-include "ground/relocation/tr_compose.ma".
-
-(* BASIC UNWIND MAP FOR PATH ************************************************)
-
-rec definition unwind1_rmap p on p: tr_map ≝
-match p with
-[ list_empty     ⇒ 𝐢
-| list_lcons l q ⇒
-  match l with
-  [ label_d n ⇒ (unwind1_rmap q)∘𝐮❨n❩
-  | label_m   ⇒ unwind1_rmap q
-  | label_L   ⇒ ⫯(unwind1_rmap q)
-  | label_A   ⇒ unwind1_rmap q
-  | label_S   ⇒ unwind1_rmap q
-  ]
-].
-
-interpretation
-  "basic unwind map (reversed path)"
-  'BlackRightTriangle p = (unwind1_rmap p).
-
-(* Basic constructions *******************************************************)
-
-lemma unwind1_rmap_empty:
-      (𝐢) = ▶(𝐞).
-// qed.
-
-lemma unwind1_rmap_d_sn (p) (n:pnat):
-      (▶p∘𝐮❨n❩) = ▶(𝗱n◗p).
-// qed.
-
-lemma unwind1_rmap_m_sn (p):
-      ▶p = ▶(𝗺◗p).
-// qed.
-
-lemma unwind1_rmap_L_sn (p):
-      (⫯▶p) = ▶(𝗟◗p).
-// qed.
-
-lemma unwind1_rmap_A_sn (p):
-      ▶p = ▶(𝗔◗p).
-// qed.
-
-lemma unwind1_rmap_S_sn (p):
-      ▶p = ▶(𝗦◗p).
-// qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind1_rmap_tail.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind1_rmap_tail.ma
deleted file mode 100644
index 38fb8bf83..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind1_rmap_tail.ma
+++ /dev/null
@@ -1,82 +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/unwind1_rmap.ma".
-include "delayed_updating/syntax/path_tail_depth.ma".
-include "delayed_updating/syntax/path_height.ma".
-
-(* BASIC UNWIND MAP FOR PATH ************************************************)
-
-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_plus_rplus.ma".
-include "ground/arith/nat_pred_succ.ma".
-
-definition tr_nap (f) (l:nat): nat ≝
-           ↓(f@❨↑l❩).
-
-interpretation
-  "functional non-negative application (total relocation maps)"
-  'ApplySucc f l = (tr_nap f l).
-
-lemma tr_nap_unfold (f) (l):
-      ↓(f@❨↑l❩) = f@↑❨l❩.
-// qed.
-
-lemma tr_compose_nap (f2) (f1) (l):
-      f2@↑❨f1@↑❨l❩❩ = (f2∘f1)@↑❨l❩.
-#f2 #f1 #l
-<tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
-<tr_compose_pap <npsucc_pred //
-qed.
-
-lemma tr_uni_nap (n) (m):
-      m + n = 𝐮❨n❩@↑❨m❩.
-#n #m
-<tr_nap_unfold
-<tr_uni_pap <nrplus_npsucc_sn //
-qed.
-
-lemma tr_nap_push (f):
-      ∀l. ↑(f@↑❨l❩) = (⫯f)@↑❨↑l❩.
-#f #l
-<tr_nap_unfold <tr_nap_unfold
-<tr_pap_push <pnpred_psucc //
-qed.
-
-(****)
-
-lemma unwind1_rmap_labels_L (n):
-      (𝐢) = ▶(𝗟∗∗n).
-#n @(nat_ind_succ … n) -n //
-#n #IH
-<labels_succ <unwind1_rmap_L_sn //
-qed.
-
-lemma unwind1_rmap_tail (p) (n):
-      n + ♯(↳[n]p) = (▶↳[n]p)@↑❨n❩.
-#p elim p -p //
-#l #p #IH #n @(nat_ind_succ … n) -n //
-#n #_ cases l [ #m ]
-[ <unwind1_rmap_d_sn <tail_d_sn <height_d_sn
-  <nplus_assoc >IH -IH <tr_compose_nap //
-| <unwind1_rmap_m_sn <tail_m_sn <height_m_sn //
-| <unwind1_rmap_L_sn <tail_L_sn <height_L_sn
-  <tr_nap_push <npred_succ //
-| <unwind1_rmap_A_sn <tail_A_sn <height_A_sn //
-| <unwind1_rmap_S_sn <tail_S_sn <height_S_sn //
-]
-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
new file mode 100644
index 000000000..879af2518
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap.ma
@@ -0,0 +1,103 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_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 ******************************************************)
+
+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
+  ]
+].
+
+interpretation
+  "tailed unwind map (reversed path)"
+  '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).
+// qed.
+
+lemma unwind2_rmap_m_sn (f) (p):
+      ▶[f]p = ▶[f](𝗺◗p).
+// qed.
+
+lemma unwind2_rmap_L_sn (f) (p):
+      (⫯▶[f]p) = ▶[f](𝗟◗p).
+// qed.
+
+lemma unwind2_rmap_A_sn (f) (p):
+      ▶[f]p = ▶[f](𝗔◗p).
+// qed.
+
+lemma unwind2_rmap_S_sn (f) (p):
+      ▶[f]p = ▶[f](𝗦◗p).
+// qed.
+
+(* 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 //
+]
+qed.
+
+(* Constructions with list_rcons ********************************************)
+
+lemma unwind2_rmap_d_dx (f) (p) (n:pnat):
+      ▶[f∘𝐮❨n❩]p = ▶[f](p◖𝗱n).
+// qed.
+
+lemma unwind2_rmap_m_dx (f) (p):
+      ▶[f]p = ▶[f](p◖𝗺).
+// qed.
+
+lemma unwind2_rmap_L_dx (f) (p):
+      ▶[⫯f]p = ▶[f](p◖𝗟).
+// qed.
+
+lemma unwind2_rmap_A_dx (f) (p):
+      ▶[f]p = ▶[f](p◖𝗔).
+// qed.
+
+lemma unwind2_rmap_S_dx (f) (p):
+      ▶[f]p = ▶[f](p◖𝗦).
+// qed.
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
new file mode 100644
index 000000000..cc15e01b5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_eq.ma
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground/relocation/tr_compose_eq.ma".
+include "ground/relocation/tr_pn_eq.ma".
+
+(* UNWIND MAP FOR PATH ******************************************************)
+
+(* Constructions with stream_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/
+]
+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
new file mode 100644
index 000000000..579cbd514
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.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_rmap_labels.ma".
+include "delayed_updating/unwind/nap.ma".
+include "delayed_updating/syntax/path_head_depth.ma".
+include "delayed_updating/syntax/path_height.ma".
+
+(* UNWIND MAP FOR PATH ******************************************************)
+
+(* Constructions with path_head *********************************************)
+
+lemma unwind2_rmap_head_push (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 //
+| #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 //
+  | <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 //
+  | <unwind2_rmap_A_sn <path_head_A_sn <height_A_sn //
+  | <unwind2_rmap_S_sn <path_head_S_sn <height_S_sn //
+  ]
+]
+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
new file mode 100644
index 000000000..b1ddacd6f
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_labels.ma
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "delayed_updating/unwind/unwind2_rmap.ma".
+include "delayed_updating/syntax/path_labels.ma".
+include "ground/relocation/tr_pushs.ma".
+
+(* UNWIND MAP FOR PATH ******************************************************)
+
+(* Constructions with labels ************************************************)
+
+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 //
+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
new file mode 100644
index 000000000..6a52ef2e5
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_structure.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_rmap.ma".
+include "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/syntax/path_depth.ma".
+include "ground/relocation/tr_pushs.ma".
+
+(* UNWIND MAP FOR PATH ******************************************************)
+
+(* Constructions with structure and depth ***********************************)
+
+lemma unwind2_rmap_structure (p) (f):
+      (⫯*[♭p]f) = ▶[f]⊗p.
+#p elim p -p //
+* [ #n ] #p #IH #f //
+[ <unwind2_rmap_A_sn //
+| <unwind2_rmap_S_sn //
+]
+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
new file mode 100644
index 000000000..4c592528e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen.ma
@@ -0,0 +1,86 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
new file mode 100644
index 000000000..2954be831
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_after.ma
@@ -0,0 +1,25 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground/relocation/tr_compose_pap.ma".
+
+(* GENERIC UNWIND FOR PATH **************************************************)
+
+(* Properties with tr_compose ***********************************************)
+
+lemma unwind_gen_after (f2) (f1) (p):
+      ◆[f2]◆[f1]p = ◆[f2∘f1]p.
+#f2 #f1 #p @(path_ind_unwind … p) -p //
+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
new file mode 100644
index 000000000..11ddd2d03
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_eq.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/unwind_gen.ma".
+include "ground/relocation/tr_pap_eq.ma".
+
+(* GENERIC UNWIND FOR PATH **************************************************)
+
+(* Constructions with stream_eq *********************************************)
+
+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 //
+]
+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
new file mode 100644
index 000000000..2948a913e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind_gen_structure.ma
@@ -0,0 +1,269 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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_empty_dx (n) (p) (f):
+      (⊗p)◖𝗱(f@❨n❩) = ◆[f](p◖𝗱n).
+#n #p #f <unwind_gen_append_proper_dx // 
+qed.
+
+lemma unwind_gen_m_dx (p) (f):
+      ⊗p = ◆[f](p◖𝗺).
+#p #f <unwind_gen_append_proper_dx //
+qed.
+
+lemma unwind_gen_L_dx (p) (f):
+      (⊗p)◖𝗟 = ◆[f](p◖𝗟).
+#p #f <unwind_gen_append_proper_dx //
+qed.
+
+lemma unwind_gen_A_dx (p) (f):
+      (⊗p)◖𝗔 = ◆[f](p◖𝗔).
+#p #f <unwind_gen_append_proper_dx //
+qed.
+
+lemma unwind_gen_S_dx (p) (f):
+      (⊗p)◖𝗦 = ◆[f](p◖𝗦).
+#p #f <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-.
diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 59df30532..1ec7f4878 100644
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1532,7 +1532,7 @@ let predefined_classes = [
  ["{"; "❴"; "⦃" ] ;
  ["}"; "❵"; "⦄" ] ;
  ["□"; "◽"; "▪"; "◾"; ];
- ["◊"; "⬦"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ;
+ ["◊"; "⬦"; "♢"; "◆"; "⧫"; "♦"; "⟐"; "⟠"; ] ;
  [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; "⊃"; "⊐"; ] ;
  ["≥"; "⪀"; "≽"; "⪴"; "⥸"; "⊒"; ]; 
  ["∨"; "⩖"; "∪"; "∩"; "⋓"; "⋒" ] ;
-- 
2.39.2