From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 29 Jun 2022 22:53:46 +0000 (+0200)
Subject: update in delayed_updating
X-Git-Tag: make_still_working~49^2
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=3ca651e49d422d9f9a2b793841ae526baf02065c

update in delayed_updating

+ bind condition simplified for ifr and dfr
---

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
index 193136433..e0d17a691 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
@@ -25,7 +25,7 @@ include "delayed_updating/notation/relations/black_rightarrow_df_4.ma".
 definition dfr (p) (q): relation2 prototerm prototerm ≝
            λt1,t2. ∃n:pnat.
            let r ≝ p●𝗔◗𝗟◗q in
-           ∧∧ (𝗟◗q)ᴿ = ↳[n](rᴿ) & r◖𝗱n ϵ t1 &
+           ∧∧ (𝗟◗q)ᴿ = ↳[n](𝗟◗q)ᴿ & r◖𝗱n ϵ t1 &
               t1[⋔r←𝛕n.(t1⋔(p◖𝗦))] ⇔ t2
 .
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
index e54dd2678..2b15d3d52 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -41,13 +41,12 @@ theorem dfr_des_ifr (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 →
 @(ex_intro … (↑♭q)) @and3_intro
 [ -H0t1 -Ht1 -Ht2
   >structure_L_sn >structure_reverse
-  >H1n >path_head_structure_depth <H1n -H1n //
+  >H1n in ⊢ (??%?); >path_head_structure_depth <H1n -H1n //
 | lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H0t1
-  <unwind2_path_d_dx
-  >list_append_rcons_sn in H1n; <reverse_append #H1n
-  lapply (unwind2_rmap_append_pap_closed f … H1n)
+  <unwind2_path_d_dx >(list_append_rcons_sn … p) <reverse_append
+  lapply (unwind2_rmap_append_pap_closed f … (p◖𝗔)ᴿ … H1n) -H1n
   <reverse_lcons <depth_L_dx #H2n
-  lapply (eq_inv_ninj_bi … H2n) -H2n #H2n <H2n -H2n -H1n #Ht1 //
+  lapply (eq_inv_ninj_bi … H2n) -H2n #H2n <H2n -H2n #Ht1 //
 | lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (unwind2_term_fsubst …))
@@ -58,12 +57,12 @@ theorem dfr_des_ifr (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 →
     @(subset_eq_trans … (lift_unwind2_term_after …))
     @unwind2_term_eq_repl_sn
 (* Note: crux of the proof begins *)
-    >list_append_rcons_sn in H1n; <reverse_append #H1n
+    >list_append_rcons_sn <reverse_append
     @(stream_eq_trans … (tr_compose_uni_dx …))
     @tr_compose_eq_repl
     [ <unwind2_rmap_append_pap_closed //
     | >unwind2_rmap_A_sn <reverse_rcons
-      /2 width=1 by tls_unwind2_rmap_append_closed/
+      /2 width=1 by tls_unwind2_rmap_closed/
     ]
 (* Note: crux of the proof ends *)
   | //
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 7273cd780..757497d4e 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
@@ -31,8 +31,7 @@ theorem dfr_lift_bi (f) (p) (q) (t1) (t2):
 @(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 //
+  <(lift_path_head … H1n) in ⊢ (??%?); -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
@@ -45,7 +44,7 @@ theorem dfr_lift_bi (f) (p) (q) (t1) (t2):
   @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/
+  /2 width=1 by tls_lift_rmap_closed/
 (* Note: crux of the proof ends *)
 ]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
index 8be4493b7..765387b1c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
@@ -24,7 +24,7 @@ include "delayed_updating/notation/relations/black_rightarrow_if_4.ma".
 definition ifr (p) (q): relation2 prototerm prototerm ≝
            λt1,t2. ∃n:pnat.
            let r ≝ p●𝗔◗𝗟◗q in
-           ∧∧ (𝗟◗q)ᴿ = ↳[n](rᴿ) & r◖𝗱n ϵ t1 &
+           ∧∧ (𝗟◗q)ᴿ = ↳[n](𝗟◗q)ᴿ & r◖𝗱n ϵ t1 &
               t1[⋔r←↑[𝐮❨n❩](t1⋔(p◖𝗦))] ⇔ t2
 .
 
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma
index 6eb354905..0bf09b4aa 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma
@@ -33,8 +33,7 @@ theorem ifr_lift_bi (f) (p) (q) (t1) (t2):
 @(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 //
+  <(lift_path_head … H1n) in ⊢ (??%?); -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
@@ -50,7 +49,7 @@ theorem ifr_lift_bi (f) (p) (q) (t1) (t2):
   @(stream_eq_trans … (tr_compose_uni_dx …))
   @tr_compose_eq_repl //
   >list_append_rcons_sn in H1n; #H1n >lift_rmap_A_dx
-  /2 width=1 by tls_lift_rmap_append_closed/
+  /2 width=1 by tls_lift_rmap_closed/
 (* Note: crux of the proof ends *)
 ]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
index 7d5769887..6a135ea2e 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
@@ -40,13 +40,12 @@ lemma ifr_unwind_bi (f) (p) (q) (t1) (t2):
 @(ex_intro … (↑♭q)) @and3_intro
 [ -H1t1 -H2t1 -Ht1 -Ht2
   >structure_L_sn >structure_reverse
-  >H1n >path_head_structure_depth <H1n -H1n //
+  >H1n in ⊢ (??%?); >path_head_structure_depth <H1n -H1n //
 | lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H1t1 -H2t1
-  <unwind2_path_d_dx
-  >list_append_rcons_sn in H1n; <reverse_append #H1n
-  lapply (unwind2_rmap_append_pap_closed f … H1n)
+  <unwind2_path_d_dx >(list_append_rcons_sn … p) <reverse_append
+  lapply (unwind2_rmap_append_pap_closed f … (p◖𝗔)ᴿ … H1n) -H1n
   <reverse_lcons <depth_L_dx #H2n
-  lapply (eq_inv_ninj_bi … H2n) -H2n #H2n <H2n -H2n -H1n #Ht1 //
+  lapply (eq_inv_ninj_bi … H2n) -H2n #H2n <H2n -H2n #Ht1 //
 | lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
   @(subset_eq_trans … Ht2) -t2
   @(subset_eq_trans … (unwind2_term_fsubst …))
@@ -57,12 +56,12 @@ lemma ifr_unwind_bi (f) (p) (q) (t1) (t2):
     @(subset_eq_canc_dx … (unwind2_term_after_lift …))
     @unwind2_term_eq_repl_sn
 (* Note: crux of the proof begins *)
-    >list_append_rcons_sn in H1n; <reverse_append #H1n
+    >list_append_rcons_sn <reverse_append
     @(stream_eq_trans … (tr_compose_uni_dx …))
     @tr_compose_eq_repl
     [ <unwind2_rmap_append_pap_closed //
     | >unwind2_rmap_A_sn <reverse_rcons
-      /2 width=1 by tls_unwind2_rmap_append_closed/
+      /2 width=1 by tls_unwind2_rmap_closed/
     ]
 (* Note: crux of the proof ends *)
   | //
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 772cc8d09..6bbffaa77 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
@@ -22,8 +22,8 @@ include "ground/relocation/xap.ma".
 (* Constructions with head for path *****************************************)
 
 lemma lift_path_head (f) (p) (q) (n):
-      pᴿ = ↳[n](pᴿ●qᴿ) →
-      ↳[↑[q●p]f＠❨n❩](↑[f](q●p))ᴿ = (↑[↑[q]f]p)ᴿ.
+      pᴿ = ↳[n](pᴿ) →
+      ↳[↑[q●p]f＠❨n❩](↑[↑[q]f]p)ᴿ = (↑[↑[q]f]p)ᴿ.
 #f #p @(list_ind_rcons … p) -p
 [ #q #n #H0
   <(eq_inv_path_empty_head … H0) -H0
@@ -34,33 +34,28 @@ lemma lift_path_head (f) (p) (q) (n):
     [ <reverse_rcons <path_head_d_sn #H0
       elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
       <list_append_assoc <lift_rmap_d_dx <lift_path_d_dx <reverse_rcons
-      <tr_xap_succ_nap <path_head_d_sn >tr_xap_succ_nap
-      <lift_path_d_dx >lift_rmap_append <reverse_rcons
-      <(IH … H0) -IH -H0 <tr_xap_plus //
+      <tr_xap_succ_nap <path_head_d_sn
+      <(IH … H0) in ⊢ (???%); -IH -H0 <tr_xap_plus //
     | <reverse_rcons <path_head_m_sn #H0
       elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
       <list_append_assoc <lift_rmap_m_dx <lift_path_m_dx <reverse_rcons
-      <tr_xap_succ_nap <path_head_m_sn >tr_xap_succ_nap
-      <lift_path_m_dx <reverse_rcons
-      <(IH … H0) -IH -H0 //
+      <tr_xap_succ_nap <path_head_m_sn
+      <(IH … H0) in ⊢ (???%); -IH -H0 //
     | <reverse_rcons <path_head_L_sn #H0
       elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
       <list_append_assoc <lift_rmap_L_dx <lift_path_L_dx <reverse_rcons
-      <tr_xap_succ_nap <path_head_L_sn >tr_xap_succ_nap
-      <lift_path_L_dx <reverse_rcons
-      <(IH … H0) -IH -H0 //
+      <tr_xap_succ_nap <path_head_L_sn
+      <(IH … H0) in ⊢ (???%); -IH -H0 //
     | <reverse_rcons <path_head_A_sn #H0
       elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
       <list_append_assoc <lift_rmap_A_dx <lift_path_A_dx <reverse_rcons
-      <tr_xap_succ_nap <path_head_A_sn >tr_xap_succ_nap
-      <lift_path_A_dx <reverse_rcons
-      <(IH … H0) -IH -H0 //
+      <tr_xap_succ_nap <path_head_A_sn
+      <(IH … H0) in ⊢ (???%); -IH -H0 //
     | <reverse_rcons <path_head_S_sn #H0
       elim (eq_inv_list_lcons_bi ????? H0) -H0 #_ #H0
       <list_append_assoc <lift_rmap_S_dx <lift_path_S_dx <reverse_rcons
-      <tr_xap_succ_nap <path_head_S_sn >tr_xap_succ_nap
-      <lift_path_S_dx <reverse_rcons
-      <(IH … H0) -IH -H0 //
+      <tr_xap_succ_nap <path_head_S_sn
+      <(IH … H0) in ⊢ (???%); -IH -H0 //
     ]
   ]
 ]
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 3dadf0fcd..66209d837 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
@@ -21,42 +21,40 @@ include "ground/lib/stream_eq_eq.ma".
 
 (* Constructions with path_head *********************************************)
 
-lemma tls_plus_lift_rmap_reverse_closed (f) (q) (p) (n) (k):
-      q = (↳[n]q)●p →
-      ⇂*[k]↑[pᴿ]f ≗ ⇂*[n+k]↑[qᴿ]f.
+lemma tls_plus_lift_rmap_reverse_closed (f) (q) (n) (k):
+      q = ↳[n]q →
+      ⇂*[k]f ≗ ⇂*[n+k]↑[qᴿ]f.
 #f #q elim q -q
-[ #p #n #k #Hp
-  elim (eq_inv_list_empty_append … Hp) -Hp #Hn #H0 destruct
-  <path_head_empty in Hn; #Hn
-  <(eq_inv_empty_labels … Hn) -n //
-| #l #q #IH #p #n @(nat_ind_succ … n) -n //
+[ #n #k #Hq
+  <(eq_inv_path_empty_head … Hq) -n //
+| #l #q #IH #n @(nat_ind_succ … n) -n //
   #n #_ #k cases l [ #m ]
-  [ <path_head_d_sn <list_append_lcons_sn #Hp
-    elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp <nrplus_inj_sn
+  [ <path_head_d_sn #Hq
+    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hp <nrplus_inj_sn
     <reverse_lcons
     @(stream_eq_trans … (tls_lift_rmap_d_dx …))
     >nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn <nplus_plus_comm_23
     >nsucc_unfold /2 width=1 by/
-  | <path_head_m_sn <list_append_lcons_sn #Hp
-    elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
+  | <path_head_m_sn #Hq
+    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
     <reverse_lcons <lift_rmap_m_dx /2 width=1 by/
-  | <path_head_L_sn <list_append_lcons_sn #Hp
-    elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
+  | <path_head_L_sn #Hq
+    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
     <reverse_lcons <lift_rmap_L_dx <nplus_succ_sn /2 width=1 by/
-  | <path_head_A_sn <list_append_lcons_sn #Hp
-    elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
+  | <path_head_A_sn #Hq
+    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
     <reverse_lcons <lift_rmap_A_dx /2 width=2 by/
-  | <path_head_S_sn <list_append_lcons_sn #Hp
-    elim (eq_inv_list_lcons_bi ????? Hp) -Hp #_ #Hp
+  | <path_head_S_sn #Hq
+    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
     <reverse_lcons <lift_rmap_S_dx /2 width=2 by/
   ]
 ]
 qed-.
 
-lemma tls_lift_rmap_append_closed (f) (p) (q) (n):
-      qᴿ = ↳[n](p●q)ᴿ →
-      ↑[p]f ≗ ⇂*[n]↑[p●q]f.
-#f #p #q #n #H0
->(reverse_reverse p) >(reverse_reverse q)
+lemma tls_lift_rmap_closed (f) (q) (n):
+      qᴿ = ↳[n](qᴿ) →
+      f ≗ ⇂*[n]↑[q]f.
+#f #q #n #H0
+>(reverse_reverse q)
 /2 width=1 by tls_plus_lift_rmap_reverse_closed/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
index cd21acf66..f6fbae181 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_rmap_head.ma
@@ -24,38 +24,38 @@ include "ground/arith/nat_le_plus.ma".
 (* Constructions with path_head *********************************************)
 
 lemma unwind2_rmap_head_xap_le_closed (f) (p) (q) (n) (k):
-      p = (↳[n]p)●q → k ≤ n →
-      (▶[f]p)＠❨k❩ = (▶[f]↳[n]p)＠❨k❩.
+      p = ↳[n]p → k ≤ n →
+      ▶[f](p●q)＠❨k❩ = ▶[f]↳[n](p●q)＠❨k❩.
 #f #p elim p -p
-[ #q #n #k #Hq #Hk
-  elim (eq_inv_list_empty_append … Hq) -Hq * #_ //
+[ #q #n #k #Hq
+  <(eq_inv_path_empty_head … Hq) -n #Hk
+  <(nle_inv_zero_dx … Hk) -k //
 | #l #p #IH #q #n @(nat_ind_succ … n) -n
-  [ #k #_ #Hk <(nle_inv_zero_dx … Hk) -k -IH
-   <path_head_zero <unwind2_rmap_empty //
+  [ #k #_ #Hk <(nle_inv_zero_dx … Hk) -k -IH //
   | #n #_ #k cases l [ #m ]
-    [ <path_head_d_sn <list_append_lcons_sn #Hq #Hk
+    [ <path_head_d_sn #Hq #Hk
       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
       <unwind2_rmap_d_sn <unwind2_rmap_d_sn
       <tr_compose_xap <tr_compose_xap
       @(IH … Hq) -IH -Hq (**) (* auto too slow *)
       @nle_trans [| @tr_uni_xap ]
       /2 width=1 by nle_plus_bi_dx/
-    | <path_head_m_sn <list_append_lcons_sn #Hq #Hk
+    | <path_head_m_sn #Hq #Hk
       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
       <unwind2_rmap_m_sn <unwind2_rmap_m_sn
       /2 width=2 by/
-    | <path_head_L_sn <list_append_lcons_sn #Hq
+    | <path_head_L_sn #Hq
       @(nat_ind_succ … k) -k // #k #_ #Hk
       lapply (nle_inv_succ_bi … Hk) -Hk #Hk
       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
       <unwind2_rmap_L_sn <unwind2_rmap_L_sn
       <tr_xap_push <tr_xap_push
       /3 width=2 by eq_f/
-    | <path_head_A_sn <list_append_lcons_sn #Hq #Hk
+    | <path_head_A_sn #Hq #Hk
       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
       <unwind2_rmap_A_sn <unwind2_rmap_A_sn
       /2 width=2 by/
-    | <path_head_S_sn <list_append_lcons_sn #Hq #Hk
+    | <path_head_S_sn #Hq #Hk
       elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
       <unwind2_rmap_S_sn <unwind2_rmap_S_sn
       /2 width=2 by/
@@ -64,8 +64,8 @@ lemma unwind2_rmap_head_xap_le_closed (f) (p) (q) (n) (k):
 ]
 qed-.
 
-lemma unwind2_rmap_head_append_xap_closed (f) (p) (q) (n):
-      p = ↳[n](p●q) →
+lemma unwind2_rmap_head_xap_closed (f) (p) (q) (n):
+      p = ↳[n]p →
       ▶[f](p●q)＠❨n❩ = ▶[f]↳[n](p●q)＠❨n❩.
 /2 width=2 by unwind2_rmap_head_xap_le_closed/
 qed-.
@@ -89,47 +89,45 @@ lemma unwind2_rmap_head_xap (f) (p) (n):
 qed.
 
 lemma unwind2_rmap_append_pap_closed (f) (p) (q) (n:pnat):
-      p = ↳[n](p●q) →
+      p = ↳[n]p →
       ♭p = ninj (▶[f](p●q)＠⧣❨n❩).
 #f #p #q #n #Hn
->tr_xap_ninj >Hn in ⊢ (??%?);
->(unwind2_rmap_head_append_xap_closed … Hn) -Hn
+>tr_xap_ninj >(path_head_refl_append q … Hn) in ⊢ (??%?); 
+>(unwind2_rmap_head_xap_closed … Hn) -Hn
 <path_head_depth //
 qed.
 
 lemma tls_unwind2_rmap_plus_closed (f) (p) (q) (n) (k):
-      p = (↳[n]p)●q →
-      ⇂*[k]▶[f]q ≗ ⇂*[n+k]▶[f]p.
+      p = ↳[n]p →
+      ⇂*[k]▶[f]q ≗ ⇂*[n+k]▶[f](p●q).
 #f #p elim p -p
 [ #q #n #k #Hq
-  elim (eq_inv_list_empty_append … Hq) -Hq #Hn #H0 destruct
-  <path_head_empty in Hn; #Hn
-  <(eq_inv_empty_labels … Hn) -n //
+  <(eq_inv_path_empty_head … Hq) -n //
 | #l #p #IH #q #n @(nat_ind_succ … n) -n //
   #n #_ #k cases l [ #m ]
-  [ <path_head_d_sn <list_append_lcons_sn #Hq
+  [ <path_head_d_sn #Hq
     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq <nrplus_inj_sn
     @(stream_eq_trans … (tls_unwind2_rmap_d_sn …))
     >nrplus_inj_dx >nrplus_inj_sn >nrplus_inj_sn <nplus_plus_comm_23
     /2 width=1 by/
-  | <path_head_m_sn <list_append_lcons_sn #Hq
+  | <path_head_m_sn #Hq
     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
     <unwind2_rmap_m_sn /2 width=1 by/
-  | <path_head_L_sn <list_append_lcons_sn #Hq
+  | <path_head_L_sn #Hq
     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
     <unwind2_rmap_L_sn <nplus_succ_sn /2 width=1 by/
-  | <path_head_A_sn <list_append_lcons_sn #Hq
+  | <path_head_A_sn #Hq
     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
     <unwind2_rmap_A_sn /2 width=2 by/
-  | <path_head_S_sn <list_append_lcons_sn #Hq
+  | <path_head_S_sn #Hq
     elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
     <unwind2_rmap_S_sn /2 width=2 by/
   ]
 ]
 qed-.
 
-lemma tls_unwind2_rmap_append_closed (f) (p) (q) (n):
-      p = ↳[n](p●q) →
+lemma tls_unwind2_rmap_closed (f) (p) (q) (n):
+      p = ↳[n]p →
       ▶[f]q ≗ ⇂*[n]▶[f](p●q).
 /2 width=1 by tls_unwind2_rmap_plus_closed/
 qed.