From: Ferruccio Guidi <fguidi@maelstrom.helm.cs.unibo.it>
Date: Wed, 16 Mar 2022 21:32:37 +0000 (+0100)
Subject: update in ground
X-Git-Tag: make_still_working~83
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7cb9cdbd64e1abbedf3c6af5638c42e3da3f5cea;p=helm.git

update in ground

+ some additions
---

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst_lift.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst_lift.etc
new file mode 100644
index 000000000..bf5c9b6f6
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/fsubst_lift.etc
@@ -0,0 +1,59 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/substitution/fsubst.ma".
+include "delayed_updating/substitution/lift_prototerm_eq.ma".
+include "delayed_updating/substitution/lift_structure.ma".
+include "delayed_updating/syntax/preterm.ma".
+include "delayed_updating/syntax/prototerm_proper.ma".
+
+(* FOCALIZED SUBSTITUTION ***************************************************)
+
+lemma lift_fsubst_sn (f) (t) (u) (p): u ϵ 𝐏 →
+      (↑[f]t)[⋔(⊗p)←↑[↑[p]f]u] ⊆ ↑[f](t[⋔p←u]).
+#f #t #u #p #Hu #ql * *
+[ #rl * #r #Hr #H1 #H2 destruct
+  >lift_append_proper_dx
+  /4 width=5 by in_comp_lift_bi, 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 (lift_path_root f q) #r #_ #Hr /2 width=2 by/
+  | #l #r #H2 destruct
+    @H0 -H0 [| <lift_append_proper_dx /2 width=3 by ppc_lcons/ ]
+  ]
+]
+qed-.
+
+lemma lift_fsubst_dx (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 𝐓 →
+      ↑[f](t[⋔p←u]) ⊆ (↑[f]t)[⋔(⊗p)←↑[↑[p]f]u].
+#f #t #u #p #Hu #H1p #H2p #ql * #q * *
+[ #r #Hu #H1 #H2 destruct
+  @or_introl @ex2_intro
+  [|| <lift_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_lift_bi/ ] *
+  [ <list_append_empty_dx #Hr @(H0 … (𝐞)) -H0
+    <list_append_empty_dx @H2p -H2p /2 width=1 by prototerm_in_comp_root/
+  | #l #r #Hr
+    elim (lift_inv_append_proper_dx … Hr) -Hr // #s1 #s2 #Hs1 #_ #H1 destruct
+    lapply (H2p … Hs1) -H2p -Hs1 /2 width=2 by ex_intro/
+  ]
+]
+qed-.
+
+lemma lift_fsubst (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 𝐓 →
+      (↑[f]t)[⋔(⊗p)←↑[↑[p]f]u] ⇔ ↑[f](t[⋔p←u]).
+/4 width=3 by lift_fsubst_sn, conj, lift_fsubst_dx/ qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_depth.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_depth.etc
new file mode 100644
index 000000000..bf6831e80
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_depth.etc
@@ -0,0 +1,48 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/substitution/lift.ma".
+include "delayed_updating/syntax/path_depth.ma".
+include "ground/relocation/tr_id_compose.ma".
+include "ground/relocation/tr_compose_compose.ma".
+include "ground/relocation/tr_compose_pn.ma".
+include "ground/relocation/tr_compose_eq.ma".
+include "ground/relocation/tr_pn_eq.ma".
+include "ground/lib/stream_eq_eq.ma".
+
+(* LIFT FOR PATH ***********************************************************)
+
+(* Constructions with depth ************************************************)
+
+lemma lift_rmap_decompose (p) (f):
+      ↑[p]f ≗ (⫯*[❘p❘]f)∘(↑[p]𝐢).
+#p @(list_ind_rcons … p) -p
+[ #f <lift_rmap_empty <lift_rmap_empty <tr_pushs_zero //
+| #p * [ #n ] #IH #f //
+  [ <lift_rmap_d_dx <lift_rmap_d_dx <depth_d_dx
+    @(stream_eq_trans … (tr_compose_assoc …))
+    /2 width=1 by tr_compose_eq_repl/
+  | <lift_rmap_L_dx <lift_rmap_L_dx <depth_L_dx
+    <tr_pushs_succ <tr_compose_push_bi
+    /2 width=1 by tr_push_eq_repl/
+  ]
+]
+qed.
+
+lemma lift_rmap_pap_le (f) (p) (n):
+      (↑[p]𝐢)@❨n❩ < ↑❘p❘ → (↑[p]𝐢)@❨n❩ = (↑[p]f)@❨n❩.
+#f #p #n #Hn
+>(tr_pap_eq_repl … (↑[p]f) … (lift_rmap_decompose …))
+<tr_compose_pap @tr_pap_pushs_le //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_preterm_eq.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_preterm_eq.etc
new file mode 100644
index 000000000..d2bbd15be
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_preterm_eq.etc
@@ -0,0 +1,81 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground/lib/subset_equivalence.ma".
+include "delayed_updating/syntax/preterm.ma".
+include "delayed_updating/substitution/lift_structure.ma".
+include "delayed_updating/substitution/lift_prototerm.ma".
+
+lemma pippo (p):
+      ⊗p ϵ 𝐈.
+#p @(list_ind_rcons … p) -p
+[ <structure_empty //
+| #p * [ #n ] #IH
+  [ <structure_d_dx //
+  | <structure_m_dx //
+  | <structure_L_dx //
+  | <structure_A_dx //
+  | <structure_S_dx //
+  ]
+]
+qed.
+
+(* LIFT FOR PRETERM *********************************************************)
+
+(* Constructions with subset_equivalence ************************************)
+
+lemma lift_grafted_sn (f) (t) (p): p ϵ 𝐈 →
+      ↑[↑[p]f](t⋔p) ⊆ (↑[f]t)⋔(⊗p).
+#f #t #p #Hp #q * #r #Hr #H0 destruct
+@(ex2_intro … Hr) -Hr
+<lift_append_inner_sn //
+qed-.
+
+lemma lift_grafted_dx (f) (t) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
+      (↑[f]t)⋔(⊗p) ⊆ ↑[↑[p]f](t⋔p).
+#f #t #p #H1p #H2p #Ht #q * #r #Hr #H0
+elim (lift_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_lift_bi/
+qed-.
+
+lemma lift_grafted (f) (t) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
+      ↑[↑[p]f](t⋔p) ⇔ (↑[f]t)⋔(⊗p).
+/3 width=1 by lift_grafted_sn, conj, lift_grafted_dx/ qed.
+
+
+lemma lift_grafted_S_dx (f) (t) (p): p ϵ ▵t → t ϵ 𝐓 →
+      (↑[f]t)⋔((⊗p)◖𝗦) ⊆ ↑[↑[p]f](t⋔(p◖𝗦)).
+#f #t #p #Hp #Ht #q * #r #Hr
+<list_append_rcons_sn #H0
+elim (lift_inv_append_proper_dx … (sym_eq … H0)) -H0 //
+#p0 #q0 #Hp0 #Hq0 #H0 destruct
+<(Ht … Hp0) [|*: /2 width=2 by ex_intro/ ] -p
+elim (lift_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_lift_bi/
+qed-.
+
+lemma lift_grafted_S (f) (t) (p): p ϵ ▵t → t ϵ 𝐓 →
+      ↑[↑[p]f](t⋔(p◖𝗦)) ⇔ (↑[f]t)⋔((⊗p)◖𝗦).
+#f #t #p #Hp #Ht
+@conj
+[ >lift_rmap_S_dx >structure_S_dx
+  @lift_grafted_sn //
+| /2 width=1 by lift_grafted_S_dx/
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_structure.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_structure.etc
new file mode 100644
index 000000000..2a219e0ff
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_structure.etc
@@ -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/substitution/lift_eq.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".
+
+(* LIFT FOR PATH ***********************************************************)
+
+(* Basic constructions with structure **************************************)
+
+lemma structure_lift (p) (f):
+      ⊗p = ⊗↑[f]p.
+#p @(path_ind_lift … p) -p // #p #IH #f
+<lift_path_L_sn //
+qed.
+
+lemma lift_structure (p) (f):
+      ⊗p = ↑[f]⊗p.
+#p @(path_ind_lift … p) -p //
+qed.
+
+(* Destructions with structure **********************************************)
+
+lemma lift_des_structure (q) (p) (f):
+      ⊗q = ↑[f]p → ⊗q = ⊗p.
+// qed-.
+
+(* Constructions with proper condition for path *****************************)
+
+lemma lift_append_proper_dx (p2) (p1) (f): p2 ϵ 𝐏 →
+      (⊗p1)●(↑[↑[p1]f]p2) = ↑[f](p1●p2).
+#p2 #p1 @(path_ind_lift … p1) -p1 //
+[ #n | #n #l #p1 |*: #p1 ] #IH #f #Hp2
+[ elim (ppc_inv_lcons … Hp2) -Hp2 #l #q #H destruct //
+| <lift_path_d_lcons_sn <IH //
+| <lift_path_m_sn <IH //
+| <lift_path_L_sn <IH //
+| <lift_path_A_sn <IH //
+| <lift_path_S_sn <IH //
+]
+qed-.
+
+(* Constructions with inner condition for path ******************************)
+
+lemma lift_append_inner_sn (p1) (p2) (f): p1 ϵ 𝐈 →
+      (⊗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 <lift_append_proper_dx //
+| <list_append_rcons_sn <lift_append_proper_dx //
+  <structure_L_dx <list_append_rcons_sn //
+| <list_append_rcons_sn <lift_append_proper_dx //
+  <structure_A_dx <list_append_rcons_sn //
+| <list_append_rcons_sn <lift_append_proper_dx //
+  <structure_S_dx <list_append_rcons_sn //
+]
+qed-.
+
+(* Advanced constructions with proj_path ************************************)
+
+lemma lift_path_d_empty_dx (n) (p) (f):
+      (⊗p)◖𝗱((↑[p]f)@❨n❩) = ↑[f](p◖𝗱n).
+#n #p #f <lift_append_proper_dx // 
+qed.
+
+lemma lift_path_m_dx (p) (f):
+      ⊗p = ↑[f](p◖𝗺).
+#p #f <lift_append_proper_dx //
+qed.
+
+lemma lift_path_L_dx (p) (f):
+      (⊗p)◖𝗟 = ↑[f](p◖𝗟).
+#p #f <lift_append_proper_dx //
+qed.
+
+lemma lift_path_A_dx (p) (f):
+      (⊗p)◖𝗔 = ↑[f](p◖𝗔).
+#p #f <lift_append_proper_dx //
+qed.
+
+lemma lift_path_S_dx (p) (f):
+      (⊗p)◖𝗦 = ↑[f](p◖𝗦).
+#p #f <lift_append_proper_dx //
+qed.
+
+lemma lift_path_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 with proj_path ***************************************)
+
+lemma lift_path_inv_d_sn (k) (q) (p) (f):
+      (𝗱k◗q) = ↑[f]p →
+      ∃∃r,h. 𝐞 = ⊗r & (↑[r]f)@❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
+#k #q #p @(path_ind_lift … p) -p
+[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
+[ <lift_path_empty #H destruct
+| <lift_path_d_empty_sn #H destruct -IH
+  /2 width=5 by ex4_2_intro/
+| <lift_path_d_lcons_sn #H
+  elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
+  /2 width=5 by ex4_2_intro/
+| <lift_path_m_sn #H
+  elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
+  /2 width=5 by ex4_2_intro/
+| <lift_path_L_sn #H destruct
+| <lift_path_A_sn #H destruct
+| <lift_path_S_sn #H destruct
+]
+qed-.
+
+lemma lift_path_inv_m_sn (q) (p) (f):
+      (𝗺◗q) = ↑[f]p → ⊥.
+#q #p @(path_ind_lift … p) -p
+[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
+[ <lift_path_empty #H destruct
+| <lift_path_d_empty_sn #H destruct
+| <lift_path_d_lcons_sn #H /2 width=2 by/
+| <lift_path_m_sn #H /2 width=2 by/
+| <lift_path_L_sn #H destruct
+| <lift_path_A_sn #H destruct
+| <lift_path_S_sn #H destruct
+]
+qed-.
+
+lemma lift_path_inv_L_sn (q) (p) (f):
+      (𝗟◗q) = ↑[f]p →
+      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ↑[⫯↑[r1]f]r2 & r1●𝗟◗r2 = p.
+#q #p @(path_ind_lift … p) -p
+[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
+[ <lift_path_empty #H destruct
+| <lift_path_d_empty_sn #H destruct
+| <lift_path_d_lcons_sn #H
+  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+  /2 width=5 by ex3_2_intro/
+| <lift_path_m_sn #H
+  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+  /2 width=5 by ex3_2_intro/
+| <lift_path_L_sn #H destruct -IH
+  /2 width=5 by ex3_2_intro/
+| <lift_path_A_sn #H destruct
+| <lift_path_S_sn #H destruct
+]
+qed-.
+
+lemma lift_path_inv_A_sn (q) (p) (f):
+      (𝗔◗q) = ↑[f]p →
+      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ↑[↑[r1]f]r2 & r1●𝗔◗r2 = p.
+#q #p @(path_ind_lift … p) -p
+[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
+[ <lift_path_empty #H destruct
+| <lift_path_d_empty_sn #H destruct
+| <lift_path_d_lcons_sn #H
+  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+  /2 width=5 by ex3_2_intro/
+| <lift_path_m_sn #H
+  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+  /2 width=5 by ex3_2_intro/
+| <lift_path_L_sn #H destruct
+| <lift_path_A_sn #H destruct -IH
+  /2 width=5 by ex3_2_intro/
+| <lift_path_S_sn #H destruct
+]
+qed-.
+
+lemma lift_path_inv_S_sn (q) (p) (f):
+      (𝗦◗q) = ↑[f]p →
+      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ↑[↑[r1]f]r2 & r1●𝗦◗r2 = p.
+#q #p @(path_ind_lift … p) -p
+[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
+[ <lift_path_empty #H destruct
+| <lift_path_d_empty_sn #H destruct
+| <lift_path_d_lcons_sn #H
+  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+  /2 width=5 by ex3_2_intro/
+| <lift_path_m_sn #H
+  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
+  /2 width=5 by ex3_2_intro/| <lift_path_L_sn #H destruct
+| <lift_path_A_sn #H destruct
+| <lift_path_S_sn #H destruct -IH
+  /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+(* Inversions with proper condition for path ********************************)
+
+lemma lift_inv_append_proper_dx (q2) (q1) (p) (f):
+      q2 ϵ 𝐏 → q1●q2 = ↑[f]p →
+      ∃∃p1,p2. ⊗p1 = q1 & ↑[↑[p1]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 (lift_path_inv_d_sn … H) -H #r1 #m1 #_ #_ #H0 #_ -IH
+    elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
+    elim Hq2 -Hq2 //
+  | elim (lift_path_inv_m_sn … H)
+  | elim (lift_path_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 (lift_path_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 (lift_path_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 lift_inv_append_inner_sn (q1) (q2) (p) (f):
+      q1 ϵ 𝐈 → q1●q2 = ↑[f]p →
+      ∃∃p1,p2. ⊗p1 = q1 & ↑[↑[p1]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 (lift_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+    elim (lift_path_inv_m_sn … (sym_eq … H2))
+  | <list_append_rcons_sn #H0
+    elim (lift_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+    elim (lift_path_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 (lift_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+    elim (lift_path_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 (lift_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
+    elim (lift_path_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/contribs/lambdadelta/delayed_updating/etc/lift/lift_structure_depth.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_structure_depth.etc
new file mode 100644
index 000000000..a85caab1c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_structure_depth.etc
@@ -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/substitution/lift.ma".
+include "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/syntax/path_depth.ma".
+include "ground/arith/nat_pred_succ.ma".
+
+(* LIFT FOR PATH ***********************************************************)
+
+(* Basic constructions with structure and depth ****************************)
+
+lemma lift_rmap_structure (p) (f):
+      (⫯*[❘p❘]f) = ↑[⊗p]f.
+#p elim p -p //
+* [ #n ] #p #IH #f //
+[ <lift_rmap_A_sn //
+| <lift_rmap_S_sn //
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_update.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_update.etc
new file mode 100644
index 000000000..e30fc9d19
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/lift/lift_update.etc
@@ -0,0 +1,83 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/substitution/lift_eq.ma".
+include "delayed_updating/syntax/path_update.ma".
+include "delayed_updating/syntax/path_depth.ma".
+include "ground/lib/stream_eq_eq.ma".
+
+(* LIFT FOR PATH ***********************************************************)
+
+(* Constructions with update ***********************************************)
+
+lemma lift_rmap_pap_le (f1) (f2) (p) (m:pnat) (l:nat):
+      ninj (m+⧣p+l) = ❘p❘ →
+      (↑[p]f1)@❨m❩ = (↑[p]f2)@❨m❩.
+#f1 #f2 #p @(list_ind_rcons … p) -p
+[ #m #l <depth_empty #H0 destruct
+| #p * [ #n ] #IH #m #l
+  [ <update_d_dx <depth_d_dx <lift_rmap_pap_d_dx <lift_rmap_pap_d_dx
+    <nplus_comm <nrplus_inj_sn <nrplus_inj_dx <nrplus_pplus_assoc
+    #H0 <(IH … l) -IH //
+  | /2 width=2 by/
+  | <update_L_dx <depth_L_dx <lift_rmap_L_dx <lift_rmap_L_dx
+    cases m -m // #m
+    <nrplus_succ_sn <nrplus_succ_sn >nsucc_inj #H0
+    <tr_pap_push <tr_pap_push
+    <(IH … l) -IH //
+  | /2 width=2 by/
+  | /2 width=2 by/
+  ]
+]
+qed.
+
+lemma lift_rmap_pap_gt (f) (p) (m):
+      f@❨m+⧣p❩+❘p❘ = (↑[p]f)@❨m+❘p❘❩.
+#f #p @(list_ind_rcons … p) -p [ // ]
+#p * [ #n ] #IH #m
+[ <update_d_dx <depth_d_dx
+  <nplus_comm <nrplus_inj_sn <nrplus_inj_dx <nrplus_pplus_assoc
+  <lift_rmap_pap_d_dx >IH -IH //
+| //
+| <update_L_dx <depth_L_dx
+  <nrplus_succ_dx <nrplus_succ_dx <lift_rmap_L_dx <tr_pap_push //
+| //
+| //
+]
+qed.
+
+lemma lift_rmap_tls_gt (f) (p) (m:pnat):
+      ⇂*[ninj (m+⧣p)]f ≗ ⇂*[ninj (m+❘p❘)]↑[p]f.
+#f #p @(list_ind_rcons … p) -p [ // ]
+#p * [ #n ] #IH #m
+[ <update_d_dx <depth_d_dx
+  <nplus_comm <nrplus_inj_sn <nrplus_inj_dx <nrplus_pplus_assoc
+  @(stream_eq_trans … (lift_rmap_tls_d_dx …))
+  @(stream_eq_canc_dx … (IH …)) -IH //
+| //
+| <update_L_dx <depth_L_dx
+  <nrplus_succ_dx >nsucc_inj //
+| //
+| //
+]
+qed.
+
+lemma lift_rmap_tls_eq (f) (p):
+      ⇂*[⧣p]f ≗ ⇂*[↑❘p❘]↑[p]⫯f.
+(*
+#f #p @(list_ind_rcons … p) -p //
+#p * [ #n ] #IH //
+<update_d_dx <depth_d_dx <lift_rmap_d_dx
+@(stream_eq_trans … (tr_tls_compose_uni_dx …))
+*)
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
index 7d7aa437e..54cf97875 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_compose.ma
@@ -44,8 +44,8 @@ qed.
 
 (* Main constructions with tr_compose and tr_tls ****************************)
 
-theorem tr_compose_uni_dx (f) (n):
-        (𝐮❨f@❨n❩❩∘⇂*[n]f ≗ f∘𝐮❨n❩).
+theorem tr_compose_uni_dx (f) (p):
+        (𝐮❨f@❨p❩❩∘⇂*[p]f) ≗ f∘𝐮❨p❩.
 #f #p
 @nstream_eq_inv_ext #q
 <tr_compose_pap <tr_compose_pap
diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_eq.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_eq.ma
new file mode 100644
index 000000000..b7d05284e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_uni_eq.ma
@@ -0,0 +1,24 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground/relocation/tr_uni.ma".
+include "ground/lib/stream_eq.ma".
+
+(* UNIFORM ELEMENTS FOR TOTAL RELOCATION MAPS *******************************)
+
+(* Constructions with stream_eq *********************************************)
+
+lemma tr_uni_eq_repl (n1) (n2):
+      n1 = n2 → 𝐮❨n1❩ ≗ 𝐮❨n2❩.
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index d04a95414..333416ec2 100644
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -30,7 +30,7 @@ table {
         }
       ]
       [ { "total relocation" * } {
-          [ "tr_uni ( 𝐮❨?❩ )" "tr_uni_pap" "tr_uni_compose" * ]
+          [ "tr_uni ( 𝐮❨?❩ )" "tr_uni_eq" "tr_uni_pap" "tr_uni_compose" * ]
           [ "tr_id ( 𝐢 ) " "tr_id_pushs" "tr_id_pap" "tr_id_compose" * ]
           [ "tr_compose ( ?∘? )" "tr_compose_eq" "tr_compose_tls" "tr_compose_pn" "tr_compose_pushs" "tr_compose_pap" "tr_compose_compose" * ]
           [ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_tls" "tr_pap_pat" "tr_pap_pn" "tr_pap_pushs" "tr_pap_pap" * ]