From e4328f6887dc0235d49d965a5ba44787b1754b80 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 14 Aug 2022 18:02:46 +0200
Subject: [PATCH] update in delayed_updating

+ focused reduction takes just one focus
+ changed minor premise of ifr_unwind_bi
+ some renaming
---
 ...arrow_df_4.ma => black_rightarrow_df_3.ma} |  4 +-
 ...arrow_if_4.ma => black_rightarrow_if_3.ma} |  4 +-
 .../delayed_updating/reduction/dfr.ma         | 16 +++--
 .../delayed_updating/reduction/dfr_ifr.ma     | 15 ++--
 .../delayed_updating/reduction/dfr_lift.ma    | 15 ++--
 .../delayed_updating/reduction/ifr.ma         | 16 +++--
 .../delayed_updating/reduction/ifr_lift.ma    | 13 ++--
 .../delayed_updating/reduction/ifr_unwind.ma  | 22 +++---
 .../syntax/prototerm_proper_inner.ma          |  2 +-
 .../unwind/unwind2_path_append.ma             | 68 +++++++++----------
 .../unwind/unwind2_preterm_eq.ma              |  6 +-
 .../unwind/unwind2_preterm_fsubst.ma          | 57 +++++++++++++---
 .../unwind/unwind2_prototerm_inner.ma         |  6 +-
 13 files changed, 146 insertions(+), 98 deletions(-)
 rename matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/{black_rightarrow_df_4.ma => black_rightarrow_df_3.ma} (89%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/{black_rightarrow_if_4.ma => black_rightarrow_if_3.ma} (89%)

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_df_4.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_df_3.ma
similarity index 89%
rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_df_4.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_df_3.ma
index ca059fc5c..f50962063 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_df_4.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_df_3.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR DELAYED UPDATING ********************************************)
 
-notation "hvbox( t1 ➡𝐝𝐟[ break term 46 p, break term 46 q ] break term 46 t2 )"
+notation "hvbox( t1 ➡𝐝𝐟[ break term 46 r ] break term 46 t2 )"
    non associative with precedence 45
-   for @{ 'BlackRightArrowDF $t1 $p $q $t2 }.
+   for @{ 'BlackRightArrowDF $t1 $r $t2 }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_if_4.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_if_3.ma
similarity index 89%
rename from matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_if_4.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_if_3.ma
index 2b35b91ea..d2568773a 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_if_4.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/black_rightarrow_if_3.ma
@@ -14,6 +14,6 @@
 
 (* NOTATION FOR DELAYED UPDATING ********************************************)
 
-notation "hvbox( t1 ➡𝐢𝐟[ break term 46 p, break term 46 q ] break term 46 t2 )"
+notation "hvbox( t1 ➡𝐢𝐟[ break term 46 r ] break term 46 t2 )"
    non associative with precedence 45
-   for @{ 'BlackRightArrowIF $t1 $p $q $t2 }.
+   for @{ 'BlackRightArrowIF $t1 $r $t2 }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
index 135a48b1d..a610cd323 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
@@ -17,17 +17,19 @@ include "delayed_updating/syntax/prototerm_constructors.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".
 include "delayed_updating/syntax/path_head.ma".
 include "delayed_updating/syntax/path_depth.ma".
-include "delayed_updating/notation/relations/black_rightarrow_df_4.ma".
+include "delayed_updating/notation/relations/black_rightarrow_df_3.ma".
+include "ground/xoa/ex_4_3.ma".
 
 (* DELAYED FOCUSED REDUCTION ************************************************)
 
-definition dfr (p) (q): relation2 prototerm prototerm ≝
-           λt1,t2. ∃k:pnat.
-           let r ≝ p●𝗔◗𝗟◗q in
-           ∧∧ 𝗟◗q = ↳[k](𝗟◗q) & r◖𝗱k ϵ t1 &
-              t1[⋔r←𝛕k.(t1⋔(p◖𝗦))] ⇔ t2
+(**) (* explicit ninj because we cannot declare the expectd type of k *)
+definition dfr (r): relation2 prototerm prototerm ≝
+           λt1,t2.
+           ∃∃p,q,k. p●𝗔◗𝗟◗q = r &
+           (𝗟◗q) = ↳[ninj k](𝗟◗q) & r◖𝗱k ϵ t1 &
+           t1[⋔r←𝛕k.(t1⋔(p◖𝗦))] ⇔ t2
 .
 
 interpretation
   "focused reduction with delayed updating (prototerm)"
-  'BlackRightArrowDF t1 p q t2 = (dfr p q t1 t2).
+  'BlackRightArrowDF t1 r t2 = (dfr r t1 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 638dad75b..68cea487c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -32,12 +32,13 @@ include "delayed_updating/syntax/path_structure_depth.ma".
 
 (* Main destructions with ifr ***********************************************)
 
-theorem dfr_des_ifr (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 →
-        t1 ➡𝐝𝐟[p,q] t2 → ▼[f]t1 ➡𝐢𝐟[⊗p,⊗q] ▼[f]t2.
-#f #p #q #t1 #t2 #H0t1
-* #k * #H1k #Ht1 #Ht2
-@(ex_intro … (↑♭q)) @and3_intro
-[ -H0t1 -Ht1 -Ht2
+theorem dfr_des_ifr (f) (t1) (t2) (r): t1 ϵ 𝐓 →
+        t1 ➡𝐝𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐟[⊗r] ▼[f]t2.
+#f #t1 #t2 #r #H0t1
+* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
+@(ex4_3_intro … (⊗p) (⊗q) (↑♭q))
+[ -H0t1 -H1k -Ht1 -Ht2 //
+| -H0t1 -Ht1 -Ht2
   >structure_L_sn
   >H1k in ⊢ (??%?); >path_head_structure_depth <H1k -H1k //
 | lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H0t1
@@ -47,7 +48,7 @@ theorem dfr_des_ifr (f) (p) (q) (t1) (t2): t1 ϵ 𝐓 →
   lapply (eq_inv_ninj_bi … H2k) -H2k #H2k <H2k -H2k #Ht1 //
 | lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
   @(subset_eq_trans … Ht2) -t2
-  @(subset_eq_trans … (unwind2_term_fsubst …))
+  @(subset_eq_trans … (unwind2_term_fsubst_ppc …))
   [ @fsubst_eq_repl [ // | // ]
     @(subset_eq_trans … (unwind2_term_iref …))
     @(subset_eq_canc_sn … (lift_term_eq_repl_dx …))
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 e8d26308e..71a599326 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_lift.ma
@@ -24,12 +24,15 @@ include "delayed_updating/substitution/lift_rmap_head.ma".
 
 (* Constructions with lift **************************************************)
 
-theorem dfr_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
-* #k * #H1k #Ht1 #Ht2
-@(ex_intro … ((↑[p●𝗔◗𝗟◗q]f)＠⧣❨k❩)) @and3_intro
-[ -Ht1 -Ht2
+(* ↑[↑[p◖𝗔◖𝗟]f]q *)
+
+theorem dfr_lift_bi (f) (t1) (t2) (r):
+        t1 ➡𝐝𝐟[r] t2 → ↑[f]t1 ➡𝐝𝐟[↑[f]r] ↑[f]t2.
+#f #t1 #t2 #r
+* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
+@(ex4_3_intro … (↑[f]p) (↑[↑[p◖𝗔◖𝗟]f]q) ((↑[p●𝗔◗𝗟◗q]f)＠⧣❨k❩))
+[ -H1k -Ht1 -Ht2 //
+| -Ht1 -Ht2
   <lift_rmap_L_dx >lift_path_L_sn
   <(lift_path_head_closed … H1k) in ⊢ (??%?); -H1k //
 | lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -H1k
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
index 6ded5c377..b36038141 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
@@ -16,18 +16,20 @@ include "delayed_updating/substitution/fsubst.ma".
 include "delayed_updating/substitution/lift_prototerm.ma".
 include "delayed_updating/syntax/prototerm_eq.ma".
 include "delayed_updating/syntax/path_head.ma".
-include "delayed_updating/notation/relations/black_rightarrow_if_4.ma".
+include "delayed_updating/notation/relations/black_rightarrow_if_3.ma".
 include "ground/relocation/tr_uni.ma".
+include "ground/xoa/ex_4_3.ma".
 
 (* IMMEDIATE FOCUSED REDUCTION ************************************************)
 
-definition ifr (p) (q): relation2 prototerm prototerm ≝
-           λt1,t2. ∃k:pnat.
-           let r ≝ p●𝗔◗𝗟◗q in
-           ∧∧ 𝗟◗q = ↳[k](𝗟◗q) & r◖𝗱k ϵ t1 &
-              t1[⋔r←↑[𝐮❨k❩](t1⋔(p◖𝗦))] ⇔ t2
+(**) (* explicit ninj because we cannot declare the expectd type of k *)
+definition ifr (r): relation2 prototerm prototerm ≝
+           λt1,t2.
+           ∃∃p,q,k. p●𝗔◗𝗟◗q = r &
+           (𝗟◗q) = ↳[ninj k](𝗟◗q) & r◖𝗱k ϵ t1 &
+           t1[⋔r←↑[𝐮❨ninj k❩](t1⋔(p◖𝗦))] ⇔ t2
 .
 
 interpretation
   "focused reduction with immediate updating (prototerm)"
-  'BlackRightArrowIF t1 p q t2 = (ifr p q t1 t2).
+  'BlackRightArrowIF t1 r t2 = (ifr r t1 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 59c9dcc9e..7c4d11d73 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_lift.ma
@@ -27,12 +27,13 @@ include "ground/relocation/tr_compose_eq.ma".
 
 (* 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
-* #k * #H1k #Ht1 #Ht2
-@(ex_intro … ((↑[p●𝗔◗𝗟◗q]f)＠⧣❨k❩)) @and3_intro
-[ -Ht1 -Ht2
+theorem ifr_lift_bi (f) (t1) (t2) (r):
+        t1 ➡𝐢𝐟[r] t2 → ↑[f]t1 ➡𝐢𝐟[↑[f]r] ↑[f]t2.
+#f #t1 #t2 #r
+* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
+@(ex4_3_intro … (↑[f]p) (↑[↑[p◖𝗔◖𝗟]f]q) ((↑[p●𝗔◗𝗟◗q]f)＠⧣❨k❩))
+[ -H1k -Ht1 -Ht2 //
+| -Ht1 -Ht2
   <lift_rmap_L_dx >lift_path_L_sn
   <(lift_path_head_closed … H1k) in ⊢ (??%?); -H1k //
 | lapply (in_comp_lift_path_term f … Ht1) -Ht2 -Ht1 -H1k
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 a554bdbe2..e8cc51826 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr_unwind.ma
@@ -20,7 +20,6 @@ include "delayed_updating/unwind/unwind2_prototerm_lift.ma".
 include "delayed_updating/unwind/unwind2_rmap_head.ma".
 
 include "delayed_updating/substitution/fsubst_eq.ma".
-include "delayed_updating/substitution/lift_prototerm_proper.ma".
 include "delayed_updating/substitution/lift_prototerm_eq.ma".
 
 include "delayed_updating/syntax/path_head_structure.ma".
@@ -30,23 +29,24 @@ include "delayed_updating/syntax/path_structure_depth.ma".
 
 (* Constructions with unwind2 ***********************************************)
 
-lemma ifr_unwind_bi (f) (p) (q) (t1) (t2):
-      t1 ϵ 𝐓 → t1⋔(p◖𝗦) ϵ 𝐏 →
-      t1 ➡𝐢𝐟[p,q] t2 → ▼[f]t1 ➡𝐢𝐟[⊗p,⊗q] ▼[f]t2.
-#f #p #q #t1 #t2 #H1t1 #H2t1
-* #k * #H1k #Ht1 #Ht2
-@(ex_intro … (↑♭q)) @and3_intro
-[ -H1t1 -H2t1 -Ht1 -Ht2
+lemma ifr_unwind_bi (f) (t1) (t2) (r):
+      t1 ϵ 𝐓 → r ϵ 𝐈 →
+      t1 ➡𝐢𝐟[r] t2 → ▼[f]t1 ➡𝐢𝐟[⊗r] ▼[f]t2.
+#f #t1 #t2 #r #H1t1 #H2r
+* #p #q #k #Hr #H1k #Ht1 #Ht2 destruct
+@(ex4_3_intro … (⊗p) (⊗q) (↑♭q))
+[ -H1t1 -H2r -H1k -Ht1 -Ht2 //
+| -H1t1 -H2r -Ht1 -Ht2
   >structure_L_sn
   >H1k in ⊢ (??%?); >path_head_structure_depth <H1k -H1k //
-| lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H1t1 -H2t1
+| lapply (in_comp_unwind2_path_term f … Ht1) -Ht2 -Ht1 -H1t1 -H2r
   <unwind2_path_d_dx <list_append_rcons_sn
   lapply (unwind2_rmap_append_pap_closed f … (p◖𝗔) … H1k) -H1k
   <depth_L_sn #H2k
   lapply (eq_inv_ninj_bi … H2k) -H2k #H2k <H2k -H2k #Ht1 //
 | lapply (unwind2_term_eq_repl_dx f … Ht2) -Ht2 #Ht2
   @(subset_eq_trans … Ht2) -t2
-  @(subset_eq_trans … (unwind2_term_fsubst …))
+  @(subset_eq_trans … (unwind2_term_fsubst_pic …))
   [ @fsubst_eq_repl [ // | // ]
     @(subset_eq_canc_sn … (lift_term_eq_repl_dx …))
     [ @unwind2_term_grafted_S /2 width=2 by ex_intro/ | skip ] -Ht1
@@ -64,7 +64,7 @@ lemma ifr_unwind_bi (f) (p) (q) (t1) (t2):
 (* Note: crux of the proof ends *)
   | //
   | /2 width=2 by ex_intro/
-  | /2 width=6 by lift_term_proper/
+  | //
   ]
 ]
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_inner.ma
index e3665476b..9f09200d3 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper_inner.ma
@@ -18,7 +18,7 @@ include "ground/lib/subset_overlap.ma".
 
 (* PROPER CONDITION FOR PROTOTERM *******************************************)
 
-(* Constructions with inner condition for prototerm *************************)
+(* Constructions with pic ***************************************************)
 
 lemma term_proper_outer (t):
       t ⧸≬ 𝐈 → t ϵ 𝐏.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma
index 3114e9edd..8796ce86f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_path_append.ma
@@ -19,20 +19,20 @@ include "ground/xoa/ex_4_2.ma".
 
 (* TAILED UNWIND FOR PATH ***************************************************)
 
-(* Constructions with inner condition for path ******************************)
+(* Constructions with pic ***************************************************)
 
-lemma unwind2_path_inner (f) (p):
+lemma unwind2_path_pic (f) (p):
       p ϵ 𝐈 → ⊗p = ▼[f]p.
 #f * // * // #k #q #Hq
 elim (pic_inv_d_dx … Hq)
 qed-.
 
-(* Constructions with append and inner condition for path *******************)
+(* Constructions with append and pic ****************************************)
 
-lemma unwind2_path_append_inner_sn (f) (p) (q): p ϵ 𝐈 →
+lemma unwind2_path_append_pic_sn (f) (p) (q): p ϵ 𝐈 →
       (⊗p)●(▼[▶[f]p]q) = ▼[f](p●q).
 #f #p * [ #Hp | * [ #k ] #q #_ ] //
-[ <(unwind2_path_inner … Hp) -Hp //
+[ <(unwind2_path_pic … Hp) -Hp //
 | <unwind2_path_d_dx <unwind2_path_d_dx
   /2 width=3 by trans_eq/
 | <unwind2_path_L_dx <unwind2_path_L_dx //
@@ -41,9 +41,9 @@ lemma unwind2_path_append_inner_sn (f) (p) (q): p ϵ 𝐈 →
 ]
 qed.
 
-(* Constructions with append and proper condition for path ******************)
+(* Constructions with append and ppc ****************************************)
 
-lemma unwind2_path_append_proper_dx (f) (p) (q): q ϵ 𝐏 →
+lemma unwind2_path_append_ppc_dx (f) (p) (q): q ϵ 𝐏 →
       (⊗p)●(▼[▶[f]p]q) = ▼[f](p●q).
 #f #p * [ #Hq | * [ #k ] #q #_ ] //
 [ elim (ppc_inv_empty … Hq)
@@ -63,47 +63,47 @@ lemma unwind2_path_d_empty (f) (k):
 
 lemma unwind2_path_d_lcons (f) (p) (l) (k:pnat):
       ▼[f∘𝐮❨k❩](l◗p) = ▼[f](𝗱k◗l◗p).
-#f #p #l #k <unwind2_path_append_proper_dx in ⊢ (???%); //
+#f #p #l #k <unwind2_path_append_ppc_dx in ⊢ (???%); //
 qed.
 
 lemma unwind2_path_m_sn (f) (p):
       ▼[f]p = ▼[f](𝗺◗p).
-#f #p <unwind2_path_append_inner_sn //
+#f #p <unwind2_path_append_pic_sn //
 qed.
 
 lemma unwind2_path_L_sn (f) (p):
       (𝗟◗▼[⫯f]p) = ▼[f](𝗟◗p).
-#f #p <unwind2_path_append_inner_sn //
+#f #p <unwind2_path_append_pic_sn //
 qed.
 
 lemma unwind2_path_A_sn (f) (p):
       (𝗔◗▼[f]p) = ▼[f](𝗔◗p).
-#f #p <unwind2_path_append_inner_sn //
+#f #p <unwind2_path_append_pic_sn //
 qed.
 
 lemma unwind2_path_S_sn (f) (p):
       (𝗦◗▼[f]p) = ▼[f](𝗦◗p).
-#f #p <unwind2_path_append_inner_sn //
+#f #p <unwind2_path_append_pic_sn //
 qed.
 
-(* Destructions with inner condition for path *******************************)
+(* Destructions with pic ****************************************************)
 
-lemma unwind2_path_des_inner (f) (p):
+lemma unwind2_path_des_pic (f) (p):
       ▼[f]p ϵ 𝐈 → p ϵ 𝐈.
 #f * // * [ #k ] #p //
 <unwind2_path_d_dx #H0
 elim (pic_inv_d_dx … H0)
 qed-.
 
-(* Destructions with append and inner condition for path ********************)
+(* Destructions with append and pic *****************************************)
 
-lemma unwind2_path_des_append_inner_sn (f) (p) (q1) (q2):
+lemma unwind2_path_des_append_pic_sn (f) (p) (q1) (q2):
       q1 ϵ 𝐈 → q1●q2 = ▼[f]p →
       ∃∃p1,p2. q1 = ⊗p1 & q2 = ▼[▶[f]p1]p2 & p1●p2 = p.
 #f #p #q1 * [| * [ #k ] #q2 ] #Hq1
 [ <list_append_empty_sn #H0 destruct
-  lapply (unwind2_path_des_inner … Hq1) -Hq1 #Hp
-  <(unwind2_path_inner … Hp) -Hp
+  lapply (unwind2_path_des_pic … Hq1) -Hq1 #Hp
+  <(unwind2_path_pic … Hp) -Hp
   /2 width=5 by ex3_2_intro/
 | #H0 elim (eq_inv_d_dx_unwind2_path … H0) -H0 #r #h #Hr #H1 #H2 destruct
   elim (eq_inv_append_structure … Hr) -Hr #s1 #s2 #H1 #H2 #H3 destruct
@@ -112,24 +112,24 @@ lemma unwind2_path_des_append_inner_sn (f) (p) (q1) (q2):
 | #H0 elim (eq_inv_L_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
   @(ex3_2_intro … s1 (s2●𝗟◗r2)) //
-  <unwind2_path_append_proper_dx //
+  <unwind2_path_append_ppc_dx //
   <unwind2_path_L_sn <Hr2 -Hr2 //
 | #H0 elim (eq_inv_A_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
   @(ex3_2_intro … s1 (s2●𝗔◗r2)) //
-  <unwind2_path_append_proper_dx //
+  <unwind2_path_append_ppc_dx //
   <unwind2_path_A_sn <Hr2 -Hr2 //
 | #H0 elim (eq_inv_S_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
   @(ex3_2_intro … s1 (s2●𝗦◗r2)) //
-  <unwind2_path_append_proper_dx //
+  <unwind2_path_append_ppc_dx //
   <unwind2_path_S_sn <Hr2 -Hr2 //
 ]
 qed-.
 
-(* Inversions with append and proper condition for path *********************)
+(* Inversions with append and ppc *******************************************)
 
-lemma unwind2_path_inv_append_proper_dx (f) (p) (q1) (q2):
+lemma unwind2_path_inv_append_ppc_dx (f) (p) (q1) (q2):
       q2 ϵ 𝐏 → q1●q2 = ▼[f]p →
       ∃∃p1,p2. q1 = ⊗p1 & q2 = ▼[▶[f]p1]p2 & p1●p2 = p.
 #f #p #q1 * [| * [ #k ] #q2 ] #Hq1
@@ -142,17 +142,17 @@ lemma unwind2_path_inv_append_proper_dx (f) (p) (q1) (q2):
 | #H0 elim (eq_inv_L_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
   @(ex3_2_intro … s1 (s2●𝗟◗r2)) //
-  <unwind2_path_append_proper_dx //
+  <unwind2_path_append_ppc_dx //
   <unwind2_path_L_sn <Hr2 -Hr2 //
 | #H0 elim (eq_inv_A_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
   @(ex3_2_intro … s1 (s2●𝗔◗r2)) //
-  <unwind2_path_append_proper_dx //
+  <unwind2_path_append_ppc_dx //
   <unwind2_path_A_sn <Hr2 -Hr2 //
 | #H0 elim (eq_inv_S_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #Hr2 #H0 destruct
   elim (eq_inv_append_structure … Hr1) -Hr1 #s1 #s2 #H1 #H2 #H3 destruct
   @(ex3_2_intro … s1 (s2●𝗦◗r2)) //
-  <unwind2_path_append_proper_dx //
+  <unwind2_path_append_ppc_dx //
   <unwind2_path_S_sn <Hr2 -Hr2 //
 ]
 qed-.
@@ -167,7 +167,7 @@ lemma eq_inv_d_sn_unwind2_path (f) (q) (p) (k):
   elim (eq_inv_d_dx_unwind2_path … H0) -H0 #r1 #r2 #Hr1 #H1 #H2 destruct
   /2 width=5 by ex4_2_intro/
 | >list_cons_comm #H0
-  elim (unwind2_path_inv_append_proper_dx … H0) -H0 // #r1 #r2 #Hr1 #_ #_ -r2
+  elim (unwind2_path_inv_append_ppc_dx … H0) -H0 // #r1 #r2 #Hr1 #_ #_ -r2
   elim (eq_inv_d_dx_structure … Hr1)
 ]
 qed-.
@@ -176,7 +176,7 @@ lemma eq_inv_m_sn_unwind2_path (f) (q) (p):
       (𝗺◗q) = ▼[f]p → ⊥.
 #f #q #p
 >list_cons_comm #H0
-elim (unwind2_path_des_append_inner_sn … H0) <list_cons_comm in H0; //
+elim (unwind2_path_des_append_pic_sn … H0) <list_cons_comm in H0; //
 #H0 #r1 #r2 #Hr1 #H1 #H2 destruct
 elim (eq_inv_m_dx_structure … Hr1)
 qed-.
@@ -186,11 +186,11 @@ lemma eq_inv_L_sn_unwind2_path (f) (q) (p):
       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[⫯▶[f]r1]r2 & r1●𝗟◗r2 = p.
 #f #q #p
 >list_cons_comm #H0
-elim (unwind2_path_des_append_inner_sn … H0) <list_cons_comm in H0; //
+elim (unwind2_path_des_append_pic_sn … H0) <list_cons_comm in H0; //
 #H0 #r1 #r2 #Hr1 #H1 #H2 destruct
 elim (eq_inv_L_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
 <list_append_assoc in H0; <list_append_assoc
-<unwind2_path_append_proper_dx //
+<unwind2_path_append_ppc_dx //
 <unwind2_path_L_sn <H1 <list_append_empty_dx #H0
 elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
 /2 width=5 by ex3_2_intro/
@@ -201,11 +201,11 @@ lemma eq_inv_A_sn_unwind2_path (f) (q) (p):
       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▶[f]r1]r2 & r1●𝗔◗r2 = p.
 #f #q #p
 >list_cons_comm #H0
-elim (unwind2_path_des_append_inner_sn … H0) <list_cons_comm in H0; //
+elim (unwind2_path_des_append_pic_sn … H0) <list_cons_comm in H0; //
 #H0 #r1 #r2 #Hr1 #H1 #H2 destruct
 elim (eq_inv_A_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
 <list_append_assoc in H0; <list_append_assoc
-<unwind2_path_append_proper_dx //
+<unwind2_path_append_ppc_dx //
 <unwind2_path_A_sn <H1 <list_append_empty_dx #H0
 elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
 /2 width=5 by ex3_2_intro/
@@ -216,11 +216,11 @@ lemma eq_inv_S_sn_unwind2_path (f) (q) (p):
       ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▶[f]r1]r2 & r1●𝗦◗r2 = p.
 #f #q #p
 >list_cons_comm #H0
-elim (unwind2_path_des_append_inner_sn … H0) <list_cons_comm in H0; //
+elim (unwind2_path_des_append_pic_sn … H0) <list_cons_comm in H0; //
 #H0 #r1 #r2 #Hr1 #H1 #H2 destruct
 elim (eq_inv_S_dx_structure … Hr1) -Hr1 #s1 #s2 #H1 #_ #H3 destruct
 <list_append_assoc in H0; <list_append_assoc
-<unwind2_path_append_proper_dx //
+<unwind2_path_append_ppc_dx //
 <unwind2_path_S_sn <H1 <list_append_empty_dx #H0
 elim (eq_inv_list_rcons_bi ????? H0) -H0 #H0 #_
 /2 width=5 by ex3_2_intro/
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_eq.ma
index 57a17a894..a78d4b9ed 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_eq.ma
@@ -26,13 +26,13 @@ lemma unwind2_term_grafted_sn (f) (t) (p): p ϵ 𝐈 →
       ▼[▶[f]p](t⋔p) ⊆ (▼[f]t)⋔(⊗p).
 #f #t #p #Hp #q * #r #Hr #H0 destruct
 @(ex2_intro … Hr) -Hr
-<unwind2_path_append_inner_sn //
+<unwind2_path_append_pic_sn //
 qed-.
 
 lemma unwind2_term_grafted_dx (f) (t) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
       (▼[f]t)⋔(⊗p) ⊆ ▼[▶[f]p](t⋔p).
 #f #t #p #H1p #H2p #Ht #q * #r #Hr #H0
-elim (unwind2_path_des_append_inner_sn … (sym_eq … H0)) -H0 //
+elim (unwind2_path_des_append_pic_sn … (sym_eq … H0)) -H0 //
 #p0 #q0 #Hp0 #Hq0 #H0 destruct
 >(Ht … Hp0) [|*: /2 width=2 by ex_intro/ ] -p
 /2 width=1 by in_comp_unwind2_path_term/
@@ -46,7 +46,7 @@ lemma unwind2_term_grafted_S_dx (f) (t) (p): p ϵ ▵t → t ϵ 𝐓 →
       (▼[f]t)⋔((⊗p)◖𝗦) ⊆ ▼[▶[f]p](t⋔(p◖𝗦)).
 #f #t #p #Hp #Ht #q * #r #Hr
 >list_append_rcons_sn #H0
-elim (unwind2_path_inv_append_proper_dx … (sym_eq … H0)) -H0 //
+elim (unwind2_path_inv_append_ppc_dx … (sym_eq … H0)) -H0 //
 #p0 #q0 #Hp0 #Hq0 #H0 destruct
 >(Ht … Hp0) [|*: /2 width=2 by ex_intro/ ] -p
 elim (eq_inv_S_sn_unwind2_path … Hq0) -Hq0
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma
index 19634dccc..ecf0eaf0f 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_preterm_fsubst.ma
@@ -20,30 +20,69 @@ include "delayed_updating/syntax/prototerm_proper.ma".
 
 (* TAILED UNWIND FOR PRETERM ************************************************)
 
-(* Constructions with fsubst ************************************************)
+(* Constructions with fsubst and pic ****************************************)
 
-lemma unwind2_term_fsubst_sn (f) (t) (u) (p): u ϵ 𝐏 →
+lemma unwind2_term_fsubst_pic_sn (f) (t) (u) (p): p ϵ 𝐈 →
+      (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u] ⊆ ▼[f](t[⋔p←u]).
+#f #t #u #p #Hp #ql * *
+[ #rl * #r #Hr #H1 #H2 destruct
+  >unwind2_path_append_pic_sn
+  /4 width=3 by in_comp_unwind2_path_term, or_introl, ex2_intro/
+| * #q #Hq #H1 #H0
+  @(ex2_intro … H1) @or_intror @conj // *
+  [ <list_append_empty_sn #H2 destruct
+    elim (unwind2_path_root f q) #r #_ #Hr /2 width=2 by/
+  | #l #r #H2 destruct
+    /3 width=2 by unwind2_path_append_pic_sn/
+  ]
+]
+qed-.
+
+lemma unwind2_term_fsubst_pic_dx (f) (t) (u) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
+      ▼[f](t[⋔p←u]) ⊆ (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u].
+#f #t #u #p #Hp #H1p #H2p #ql * #q * *
+[ #r #Hu #H1 #H2 destruct
+  /5 width=3 by unwind2_path_append_pic_sn, ex2_intro, or_introl/
+| #Hq #H0 #H1 destruct
+  @or_intror @conj [ /2 width=1 by in_comp_unwind2_path_term/ ] *
+  [ <list_append_empty_sn #Hr @(H0 … (𝐞)) -H0
+    <list_append_empty_sn @H2p -H2p
+    /2 width=2 by unwind2_path_des_structure, prototerm_in_comp_root/
+  | #l #r #Hr
+    elim (unwind2_path_inv_append_ppc_dx … Hr) -Hr // #s1 #s2 #Hs1 #_ #H1 destruct
+    lapply (H2p … Hs1) -H2p -Hs1 /2 width=2 by ex_intro/
+  ]
+]
+qed-.
+
+lemma unwind2_term_fsubst_pic (f) (t) (u) (p): p ϵ 𝐈 → p ϵ ▵t → t ϵ 𝐓 →
+      (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u] ⇔ ▼[f](t[⋔p←u]).
+/4 width=3 by unwind2_term_fsubst_pic_sn, conj, unwind2_term_fsubst_pic_dx/ qed.
+
+(* Constructions with fsubst and ppc ****************************************)
+
+lemma unwind2_term_fsubst_ppc_sn (f) (t) (u) (p): u ϵ 𝐏 →
       (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u] ⊆ ▼[f](t[⋔p←u]).
 #f #t #u #p #Hu #ql * *
 [ #rl * #r #Hr #H1 #H2 destruct
-  >unwind2_path_append_proper_dx
+  >unwind2_path_append_ppc_dx
   /4 width=5 by in_comp_unwind2_path_term, in_comp_tpc_trans, or_introl, ex2_intro/
 | * #q #Hq #H1 #H0
   @(ex2_intro … H1) @or_intror @conj // *
   [ <list_append_empty_sn #H2 destruct
     elim (unwind2_path_root f q) #r #_ #Hr /2 width=2 by/
   | #l #r #H2 destruct
-    @H0 -H0 [| <unwind2_path_append_proper_dx /2 width=3 by ppc_rcons/ ]
+    @H0 -H0 [| <unwind2_path_append_ppc_dx /2 width=3 by ppc_rcons/ ]
   ]
 ]
 qed-.
 
-lemma unwind2_term_fsubst_dx (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 𝐓 →
+lemma unwind2_term_fsubst_ppc_dx (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 𝐓 →
       ▼[f](t[⋔p←u]) ⊆ (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u].
 #f #t #u #p #Hu #H1p #H2p #ql * #q * *
 [ #r #Hu #H1 #H2 destruct
   @or_introl @ex2_intro
-  [|| <unwind2_path_append_proper_dx /2 width=5 by in_comp_tpc_trans/ ]
+  [|| <unwind2_path_append_ppc_dx /2 width=5 by in_comp_tpc_trans/ ]
   /2 width=3 by ex2_intro/
 | #Hq #H0 #H1 destruct
   @or_intror @conj [ /2 width=1 by in_comp_unwind2_path_term/ ] *
@@ -51,12 +90,12 @@ lemma unwind2_term_fsubst_dx (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 
     <list_append_empty_sn @H2p -H2p
     /2 width=2 by unwind2_path_des_structure, prototerm_in_comp_root/
   | #l #r #Hr
-    elim (unwind2_path_inv_append_proper_dx … Hr) -Hr // #s1 #s2 #Hs1 #_ #H1 destruct
+    elim (unwind2_path_inv_append_ppc_dx … Hr) -Hr // #s1 #s2 #Hs1 #_ #H1 destruct
     lapply (H2p … Hs1) -H2p -Hs1 /2 width=2 by ex_intro/
   ]
 ]
 qed-.
 
-lemma unwind2_term_fsubst (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 𝐓 →
+lemma unwind2_term_fsubst_ppc (f) (t) (u) (p): u ϵ 𝐏 → p ϵ ▵t → t ϵ 𝐓 →
       (▼[f]t)[⋔(⊗p)←▼[▶[f]p]u] ⇔ ▼[f](t[⋔p←u]).
-/4 width=3 by unwind2_term_fsubst_sn, conj, unwind2_term_fsubst_dx/ qed.
+/4 width=3 by unwind2_term_fsubst_ppc_sn, conj, unwind2_term_fsubst_ppc_dx/ qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma
index cbb32a8b5..6ad293f09 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind2_prototerm_inner.ma
@@ -18,11 +18,11 @@ include "ground/lib/subset_overlap.ma".
 
 (* TAILED UNWIND FOR PROTOTERM **********************************************)
 
-(* Destructions with inner condition for path *******************************)
+(* Destructions with pic ****************************************************)
 
-lemma unwind2_term_des_inner (f) (t):
+lemma unwind2_term_des_pic (f) (t):
       ▼[f]t ≬ 𝐈 → t ≬ 𝐈.
 #f #t * #p * #q #Hq #H0 #Hp destruct
 @(subset_ol_i … Hq) -Hq (**) (* auto does not work *)
-@(unwind2_path_des_inner … Hp)
+@(unwind2_path_des_pic … Hp)
 qed-.
-- 
2.39.2