From a4cacf8e269910184348a037106551dbc8a46fd4 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 23 Jun 2022 12:54:36 +0200
Subject: [PATCH] update in delayed_updating

+ unwind2_path_after_lift
+ prelift
+ refactoring for lift
---
 .../delayed_updating/reduction/dfr_lift.ma    |  1 -
 .../delayed_updating/reduction/ifr_lift.ma    | 55 +++++++++++++++++++
 .../substitution/{lift.ma => lift_gen.ma}     |  0
 .../{lift_eq.ma => lift_gen_eq.ma}            |  2 +-
 .../substitution/lift_path_after.ma           |  2 +-
 .../substitution/lift_path_head.ma            |  2 +-
 .../{lift_id.ma => lift_path_id.ma}           | 10 +---
 .../substitution/lift_path_length.ma          |  2 +-
 .../substitution/lift_path_prelift.ma         | 31 +++++++++++
 .../substitution/lift_path_proper.ma          |  2 +-
 .../substitution/lift_path_structure.ma       |  2 +-
 .../substitution/lift_path_uni.ma             |  2 +-
 .../substitution/lift_prototerm.ma            |  2 +-
 .../substitution/lift_prototerm_id.ma         |  2 +-
 .../substitution/lift_rmap_head.ma            |  2 +-
 .../substitution/lift_rmap_id.ma              | 26 +++++++++
 .../substitution/prelift_label.ma             | 54 ++++++++++++++++++
 .../substitution/prelift_rmap.ma              | 55 +++++++++++++++++++
 .../unwind/unwind2_path_lift.ma               | 22 +++++++-
 .../unwind/unwind2_prototerm_lift.ma          | 12 +++-
 20 files changed, 261 insertions(+), 25 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma
 rename matita/matita/contribs/lambdadelta/delayed_updating/substitution/{lift.ma => lift_gen.ma} (100%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/substitution/{lift_eq.ma => lift_gen_eq.ma} (99%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/substitution/{lift_id.ma => lift_path_id.ma} (86%)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_prelift.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_id.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
index 9fbf809b3..f71d6974e 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
@@ -13,7 +13,6 @@
 (**************************************************************************)
 
 include "delayed_updating/reduction/dfr.ma".
-include "delayed_updating/reduction/ifr.ma".
 
 include "delayed_updating/substitution/fsubst_lift.ma".
 include "delayed_updating/substitution/fsubst_eq.ma".
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma
new file mode 100644
index 000000000..6d5cb47f0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma
@@ -0,0 +1,55 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "delayed_updating/reduction/ifr.ma".
+
+include "delayed_updating/unwind/unwind2_path_lift.ma".
+
+include "delayed_updating/substitution/fsubst_lift.ma".
+include "delayed_updating/substitution/fsubst_eq.ma".
+include "delayed_updating/substitution/lift_prototerm_eq.ma".
+include "delayed_updating/substitution/lift_path_head.ma".
+include "delayed_updating/substitution/lift_rmap_head.ma".
+
+(* IMMEDIATE FOCUSED REDUCTION **********************************************)
+
+(* Constructions with lift **************************************************)
+
+theorem ifr_lift_bi (f) (p) (q) (t1) (t2):
+        t1 ➡𝐢𝐟[p,q] t2 → ↑[f]t1 ➡𝐢𝐟[↑[f]p,↑[↑[p◖𝗔◖𝗟]f]q] ↑[f]t2.
+#f #p #q #t1 #t2
+* #n * #H1n #Ht1 #Ht2
+@(ex_intro … ((↑[p●𝗔◗𝗟◗q]f)＠⧣❨n❩)) @and3_intro
+[ -Ht1 -Ht2
+  <lift_rmap_L_dx >lift_path_L_sn
+  >list_append_rcons_sn in H1n; <reverse_append #H1n
+  <(lift_path_head … H1n) -H1n //
+| lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -H1n
+  <lift_path_d_dx #Ht1 //
+| lapply (lift_term_eq_repl_dx f … Ht2) -Ht2 #Ht2 -Ht1
+  @(subset_eq_trans … Ht2) -t2
+  @(subset_eq_trans … (lift_term_fsubst …))
+  @fsubst_eq_repl [ // | <lift_path_append // ]
+(*  
+  @(subset_eq_trans … (lift_term_iref …))
+  @iref_eq_repl
+  @(subset_eq_canc_sn … (lift_term_grafted_S …))
+  @lift_term_eq_repl_sn
+(* Note: crux of the proof begins *)
+  >list_append_rcons_sn in H1n; #H1n >lift_rmap_A_dx
+  /2 width=1 by tls_lift_rmap_append_closed/
+(* Note: crux of the proof ends *)
+]
+qed.
+*)
\ No newline at end of file
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_gen.ma
similarity index 100%
rename from matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_gen.ma
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_gen_eq.ma
similarity index 99%
rename from matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_gen_eq.ma
index 317e1f424..e589276a8 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_gen_eq.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/substitution/lift.ma".
+include "delayed_updating/substitution/lift_gen.ma".
 include "ground/relocation/tr_pap_pap.ma".
 include "ground/relocation/tr_pap_eq.ma".
 include "ground/relocation/tr_pn_eq.ma".
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_after.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_after.ma
index 869d680fe..1bdf3c592 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_after.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_after.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/substitution/lift_eq.ma".
+include "delayed_updating/substitution/lift_gen_eq.ma".
 include "ground/relocation/tr_compose_pap.ma".
 include "ground/relocation/tr_compose_pn.ma".
 include "ground/relocation/tr_compose_tls.ma".
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_head.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_head.ma
index 71b11f5d6..772cc8d09 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_head.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_head.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/substitution/lift_eq.ma".
+include "delayed_updating/substitution/lift_gen_eq.ma".
 include "delayed_updating/syntax/path_head.ma".
 include "delayed_updating/syntax/path_reverse.ma".
 include "ground/relocation/xap.ma".
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_id.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_id.ma
similarity index 86%
rename from matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_id.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_id.ma
index c2376b52e..cac770811 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_id.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_id.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/substitution/lift_eq.ma".
+include "delayed_updating/substitution/lift_gen_eq.ma".
 include "ground/relocation/tr_id_pap.ma".
 include "ground/relocation/tr_id_tls.ma".
 
@@ -28,11 +28,3 @@ lemma lift_path_id (p):
 | <lift_path_L_sn //
 ]
 qed.
-
-(* Constructions with proj_rmap and tr_id ***********************************)
-
-lemma lift_rmap_id (p):
-      (𝐢) = ↑[p]𝐢.
-#p elim p -p //
-* [ #n ] #p #IH //
-qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_length.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_length.ma
index a4b81aeeb..755f8d16e 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_length.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_length.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/substitution/lift_eq.ma".
+include "delayed_updating/substitution/lift_gen_eq.ma".
 include "ground/lib/list_length.ma".
 
 (* LIFT FOR PATH ************************************************************)
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_prelift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_prelift.ma
new file mode 100644
index 000000000..345f437ab
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_prelift.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/substitution/lift_gen_eq.ma".
+include "delayed_updating/substitution/prelift_label.ma".
+include "delayed_updating/substitution/prelift_rmap.ma".
+
+(* LIFT FOR PATH ************************************************************)
+
+(* Constructions with prelift_rmap and prelift_path *************************)
+
+lemma lift_path_lcons_prelift (f) (p) (l):
+      (↑[f]l)◗↑[↑[l]f]p = ↑[f](l◗p).
+#f #p * [ #n ] //
+qed.
+
+lemma lift_path_rcons_prelift (f) (p) (l):
+      (↑[f]p)◖↑[↑[p]f]l = ↑[f](p◖l).
+#f #p * [ #n ] //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_proper.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_proper.ma
index 0eef97896..1473e819f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_proper.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_proper.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/substitution/lift_eq.ma".
+include "delayed_updating/substitution/lift_gen_eq.ma".
 include "delayed_updating/syntax/path_proper.ma".
 
 (* LIFT FOR PATH ************************************************************)
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_structure.ma
index 773749b63..ece3e93e6 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_structure.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/substitution/lift_eq.ma".
+include "delayed_updating/substitution/lift_gen_eq.ma".
 include "delayed_updating/syntax/path_structure.ma".
 
 (* LIFT FOR PATH ************************************************************)
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_uni.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_uni.ma
index 0e22a3d39..f68010b32 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_uni.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_path_uni.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/substitution/lift_id.ma".
+include "delayed_updating/substitution/lift_path_id.ma".
 include "ground/relocation/tr_uni_pap.ma".
 include "ground/relocation/tr_uni_tls.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma
index ed5fbe84c..85aa8a0bb 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/substitution/lift.ma".
+include "delayed_updating/substitution/lift_gen.ma".
 include "delayed_updating/syntax/prototerm.ma".
 include "ground/lib/subset_ext.ma".
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_id.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_id.ma
index 7343319f4..11e39983b 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_id.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm_id.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "delayed_updating/substitution/lift_prototerm_eq.ma".
-include "delayed_updating/substitution/lift_id.ma".
+include "delayed_updating/substitution/lift_path_id.ma".
 
 (* LIFT FOR PROTOTERM *******************************************************)
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_head.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_head.ma
index 122262026..3dadf0fcd 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_head.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_head.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/substitution/lift_eq.ma".
+include "delayed_updating/substitution/lift_gen_eq.ma".
 include "delayed_updating/syntax/path_head.ma".
 include "delayed_updating/syntax/path_reverse.ma".
 include "ground/lib/stream_eq_eq.ma".
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_id.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_id.ma
new file mode 100644
index 000000000..077f90747
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_rmap_id.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/substitution/lift_gen.ma".
+include "ground/relocation/tr_id_tls.ma".
+
+(* LIFT FOR RELOCATION MAP  *************************************************)
+
+(* Constructions with proj_rmap and tr_id ***********************************)
+
+lemma lift_rmap_id (p):
+      (𝐢) = ↑[p]𝐢.
+#p elim p -p //
+* [ #n ] #p #IH //
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label.ma
new file mode 100644
index 000000000..e4a9c0596
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_label.ma
@@ -0,0 +1,54 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/notation/functions/uparrow_2.ma".
+include "delayed_updating/syntax/label.ma".
+include "ground/relocation/tr_pap.ma".
+
+(* PRELIFT FOR LABEL ********************************************************)
+
+definition prelift_label (f) (l): label ≝
+match l with
+[ label_d n ⇒ 𝗱(f＠⧣❨n❩)
+| label_m   ⇒ 𝗺
+| label_L   ⇒ 𝗟
+| label_A   ⇒ 𝗔
+| label_S   ⇒ 𝗦
+].
+
+interpretation
+  "prelift (label)"
+  'UpArrow f l = (prelift_label f l).
+
+(* Basic constructions ******************************************************)
+
+lemma prelift_label_d (f) (n):
+      (𝗱(f＠⧣❨n❩)) = ↑[f]𝗱n.
+// qed.
+
+lemma prelift_label_m (f):
+      (𝗺) = ↑[f]𝗺.
+// qed.
+
+lemma prelift_label_L (f):
+      (𝗟) = ↑[f]𝗟.
+// qed.
+
+lemma prelift_label_A (f):
+      (𝗔) = ↑[f]𝗔.
+// qed.
+
+lemma prelift_label_S (f):
+      (𝗦) = ↑[f]𝗦.
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap.ma
new file mode 100644
index 000000000..de7f40321
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap.ma
@@ -0,0 +1,55 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "delayed_updating/notation/functions/uparrow_2.ma".
+include "delayed_updating/syntax/label.ma".
+include "ground/relocation/tr_pn.ma".
+include "ground/lib/stream_tls.ma".
+
+(* PRELIFT FOR RELOCATION MAP ***********************************************)
+
+definition prelift_rmap (f) (l): tr_map ≝
+match l with
+[ label_d n ⇒ ⇂*[n]f
+| label_m   ⇒ f
+| label_L   ⇒ ⫯f
+| label_A   ⇒ f
+| label_S   ⇒ f
+].
+
+interpretation
+  "prelift (relocation map)"
+  'UpArrow l f = (prelift_rmap f l).
+
+(* Basic constructions ******************************************************)
+
+lemma prelift_rmap_d (f) (n:pnat):
+      ⇂*[n]f = ↑[𝗱n]f.
+// qed.
+
+lemma prelift_rmap_m (f):
+      f = ↑[𝗺]f.
+// qed.
+
+lemma prelift_rmap_L (f):
+      (⫯f) = ↑[𝗟]f.
+// qed.
+
+lemma prelift_rmap_A (f):
+      f = ↑[𝗔]f.
+// qed.
+
+lemma prelift_rmap_S (f):
+      f = ↑[𝗦]f.
+// qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma
index 71a169dbf..ac2166a46 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_lift.ma
@@ -13,13 +13,13 @@
 (**************************************************************************)
 
 include "delayed_updating/unwind/unwind2_path_eq.ma".
-include "delayed_updating/substitution/lift_eq.ma".
+include "delayed_updating/substitution/lift_path_prelift.ma".
 
 (* UNWIND FOR PATH **********************************************************)
 
-(* Properties with lift_path ************************************************)
+(* Constructions with lift_path *********************************************)
 
-lemma unwind2_lift_path_after (p) (f1) (f2):
+lemma lift_unwind2_path_after (p) (f1) (f2):
       ↑[f2]▼[f1]p = ▼[f2∘f1]p.
 #p @(path_ind_unwind … p) -p // [ #n | #p ] #IH #f1 #f2
 [ <unwind2_path_d_empty <unwind2_path_d_empty
@@ -28,3 +28,19 @@ lemma unwind2_lift_path_after (p) (f1) (f2):
   >tr_compose_push_bi //
 ]
 qed.
+
+lemma unwind2_path_after_lift (p) (f1) (f2):
+      ▼[f2]↑[f1]p = ▼[f2∘f1]p.
+#p @(path_ind_unwind … p) -p // [ #n #l ] #p #IH #f1 #f2
+[ <lift_path_d_sn <unwind2_path_d_lcons
+  <lift_path_lcons_prelift <unwind2_path_d_lcons >lift_path_lcons_prelift
+  >IH -IH
+  >(unwind2_path_eq_repl … (tr_compose_assoc …))
+  >(unwind2_path_eq_repl … (tr_compose_assoc …))
+  <unwind2_path_after <unwind2_path_after in ⊢ (???%);
+  /3 width=1 by unwind2_path_eq_repl, eq_f/
+| <lift_path_m_sn <unwind2_path_m_sn <unwind2_path_m_sn //
+| <lift_path_L_sn <unwind2_path_L_sn <unwind2_path_L_sn 
+  >tr_compose_push_bi //
+]
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma
index 8e3d2cf2f..8d987dfb7 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_lift.ma
@@ -22,10 +22,18 @@ include "delayed_updating/unwind/unwind2_prototerm.ma".
 
 (* Constructions with lift_prototerm ****************************************)
 
-lemma unwind2_lift_term_after (f1) (f2) (t):
+lemma lift_unwind2_term_after (f1) (f2) (t):
       ↑[f2]▼[f1]t ⇔ ▼[f2∘f1]t.
 #f1 #f2 #t @subset_eq_trans
 [| @subset_inclusion_ext_f1_compose ]
 @subset_equivalence_ext_f1_exteq #p
-@unwind2_lift_path_after
+@lift_unwind2_path_after
+qed.
+
+lemma unwind2_term_after_lift (f1) (f2) (t):
+      ▼[f2]↑[f1]t ⇔ ▼[f2∘f1]t.
+#f1 #f2 #t @subset_eq_trans
+[| @subset_inclusion_ext_f1_compose ]
+@subset_equivalence_ext_f1_exteq #p
+@unwind2_path_after_lift
 qed.
-- 
2.39.2