From cfd201c62dd9b854bfb4ada648d3e556b29fac3a Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Tue, 18 Jan 2022 22:46:48 +0100
Subject: [PATCH] update in delayed_updating

+ commutation of lift and fsubst
+ preterms renamed as prototerms
---
 .../notation/relations/predicate_t_hook_1.ma  |  19 +++
 .../delayed_updating/reduction/dfr.ma         |   9 +-
 .../delayed_updating/reduction/dfr_ifr.ma     |   9 +-
 .../delayed_updating/reduction/ifr.ma         |   6 +-
 .../delayed_updating/substitution/fsubst.ma   |   9 +-
 .../substitution/fsubst_lift.ma               |  56 +++++++++
 .../delayed_updating/substitution/lift.ma     |  44 ++++---
 .../delayed_updating/substitution/lift_eq.ma  |  18 +--
 .../{lift_preterm.ma => lift_prototerm.ma}    |  12 +-
 .../substitution/lift_structure.ma            | 116 +++++++++++++++++-
 .../delayed_updating/syntax/bdd_term.ma       |  34 ++---
 .../delayed_updating/syntax/path.ma           |   1 +
 .../delayed_updating/syntax/preterm.ma        |  38 +++---
 .../delayed_updating/syntax/prototerm.ma      |  44 +++++++
 ...structors.ma => prototerm_constructors.ma} |  34 ++---
 ...quivalence.ma => prototerm_equivalence.ma} |  12 +-
 .../syntax/prototerm_proper.ma                |  35 ++++++
 17 files changed, 376 insertions(+), 120 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_t_hook_1.ma
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
 rename matita/matita/contribs/lambdadelta/delayed_updating/substitution/{lift_preterm.ma => lift_prototerm.ma} (79%)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm.ma
 rename matita/matita/contribs/lambdadelta/delayed_updating/syntax/{preterm_constructors.ma => prototerm_constructors.ma} (73%)
 rename matita/matita/contribs/lambdadelta/delayed_updating/syntax/{preterm_equivalence.ma => prototerm_equivalence.ma} (81%)
 create mode 100644 matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper.ma

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_t_hook_1.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_t_hook_1.ma
new file mode 100644
index 000000000..34af172fb
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/notation/relations/predicate_t_hook_1.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* NOTATION FOR DELAYED UPDATING ********************************************)
+
+notation "hvbox( Ƭ term 70 x )"
+  non associative with precedence 45
+  for @{ 'PredicateTHook $x }.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
index 3dca53142..ed077ae2c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr.ma
@@ -15,17 +15,18 @@
 include "delayed_updating/syntax/path_depth.ma".
 include "delayed_updating/syntax/path_structure.ma".
 include "delayed_updating/syntax/path_balanced.ma".
+include "delayed_updating/syntax/prototerm_constructors.ma".
 include "delayed_updating/substitution/fsubst.ma".
 include "delayed_updating/notation/relations/black_rightarrow_df_4.ma".
 
 (* DELAYED FOCUSED REDUCTION ************************************************)
 
-inductive dfr (p) (q) (t): predicate preterm ≝
+inductive dfr (p) (q) (t): predicate prototerm ≝
 | dfr_beta (b):
-  let r ≝ p●𝗔◗b●𝗟◗q◖𝗱(↑❘q❘) in
-  r ϵ t → ⊓(⊗b) → dfr p q t (t[⋔r←t⋔(p◖𝗦)])
+  let r ≝ p●𝗔◗b●𝗟◗q in
+  r◖𝗱(↑❘q❘) ϵ t → ⊓(⊗b) → dfr p q t (t[⋔r←𝛗(↑❘q❘).t⋔(p◖𝗦)])
 .
 
 interpretation
-  "focused balanced reduction with delayed updating (preterm)"
+  "focused balanced reduction with delayed updating (prototerm)"
   'BlackRightArrowDF t1 p q t2 = (dfr p q 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 015958b54..9a713d1e5 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/dfr_ifr.ma
@@ -12,12 +12,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/reduction/ifr.ma".
 include "delayed_updating/reduction/dfr.ma".
+include "delayed_updating/reduction/ifr.ma".
+include "delayed_updating/substitution/fsubst_lift.ma".
 
 (* DELAYED FOCUSED REDUCTION ************************************************)
 
-lemma dfr_lift_bi (f) (p) (q) (t1) (t2):
+lemma dfr_lift_bi (f) (p) (q) (t1) (t2): Ƭt1 →
       t1 ➡𝐝𝐟[p,q] t2 → ↑[f]t1 ➡𝐟[⊗p,⊗q] ↑[f]t2.
-#f #p #q #t1 #t2
-* #b #Hr #Hb
+#f #p #q #t1 #t2 #Ht1
+* -t2 #b #Hr #Hb
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
index 746def177..d087bdbb7 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/reduction/ifr.ma
@@ -16,17 +16,17 @@ include "delayed_updating/syntax/path_depth.ma".
 include "delayed_updating/syntax/path_structure.ma".
 include "delayed_updating/syntax/path_balanced.ma".
 include "delayed_updating/substitution/fsubst.ma".
-include "delayed_updating/substitution/lift_preterm.ma".
+include "delayed_updating/substitution/lift_prototerm.ma".
 include "delayed_updating/notation/relations/black_rightarrow_f_4.ma".
 
 (* IMMEDIATE FOCUSED REDUCTION ************************************************)
 
-inductive ifr (p) (q) (t): predicate preterm ≝
+inductive ifr (p) (q) (t): predicate prototerm ≝
 | ifr_beta (b):
   let r ≝ p●𝗔◗b●𝗟◗q in
   r◖𝗱(↑❘q❘) ϵ t → ⊓(⊗b) → ifr p q t (t[⋔r←↑[𝐮❨↑❘q❘❩]t⋔(p◖𝗦)])
 .
 
 interpretation
-  "focused balanced reduction with immediate updating (preterm)"
+  "focused balanced reduction with immediate updating (prototerm)"
   'BlackRightArrowF t1 p q t2 = (ifr p q t1 t2).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst.ma
index 53f18be31..adbc16c04 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst.ma
@@ -12,18 +12,17 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/xoa/ex_3_1.ma".
-include "delayed_updating/syntax/preterm.ma".
+include "delayed_updating/syntax/prototerm.ma".
 include "delayed_updating/notation/functions/pitchforkleftarrow_3.ma".
 
 (* FOCALIZED SUBSTITUTION ***************************************************)
 
-definition fsubst (p) (u): preterm → preterm ≝
+definition fsubst (p) (u): prototerm → prototerm ≝
            λt,q.
-           ∨∨ ∃∃r. r ϵ u & p ϵ ▵t & p●r = q
+           ∨∨ ∃∃r. r ϵ u & p●r = q
             | ∧∧ q ϵ t & (∀r. p●r = q → ⊥)
 .
 
 interpretation
-  "focalized substitution (preterm)"
+  "focalized substitution (prototerm)"
   'PitchforkLeftArrow t p u = (fsubst p u t).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
new file mode 100644
index 000000000..c9d656028
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/fsubst_lift.ma
@@ -0,0 +1,56 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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.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 → p ⧸ϵ t →
+      (↑[f]t)[⋔(⊗p)←↑[↑[p]f]u] ⊆ ↑[f](t[⋔p←u]).
+#f #t #u #p #Hu #Hp #ql * *
+[ #rl * #r #Hr #H1 #H2 destruct
+  >lift_append_proper_dx
+  /4 width=1 by subset_in_ext_f1_dx, or_introl/
+| * #q #Hq #H1 #H0
+  @(ex2_intro … H1) @or_intror @conj //
+  #r #H2 destruct
+  @H0 -H0 [| <lift_append_proper_dx /2 width=1 by/ ]
+]
+qed-.
+
+lemma lift_fsubst_dx (f) (t) (u) (p): Ꝕu → p ϵ ▵t → structure_injective 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=1 by/ ]
+  /2 width=3 by ex2_intro/
+| #Hq #H0 #H1 destruct
+  @or_intror @conj [ /2 width=1 by subset_in_ext_f1_dx/ ] *
+  [ <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 → p ϵ ▵t → structure_injective 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/substitution/lift.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
index b1ed76623..0dbb6043a 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift.ma
@@ -21,69 +21,75 @@ include "delayed_updating/notation/functions/uparrow_2.ma".
 (* LIFT FOR PATH ***********************************************************)
 
 definition lift_continuation (A:Type[0]) ≝
-           path → tr_map → A.
+           tr_map → path → A.
 
 (* Note: inner numeric labels are not liftable, so they are removed *)
-rec definition lift_gen (A:Type[0]) (k:lift_continuation A) (p) (f) on p ≝
+rec definition lift_gen (A:Type[0]) (k:lift_continuation A) (f) (p) on p ≝
 match p with
-[ list_empty     ⇒ k (𝐞) f
+[ list_empty     ⇒ k f (𝐞)
 | list_lcons l q ⇒
   match l with
   [ label_node_d n ⇒
     match q with
-    [ list_empty     ⇒ lift_gen (A) (λp. k (𝗱(f@❨n❩)◗p)) q (f∘𝐮❨n❩)
-    | list_lcons _ _ ⇒ lift_gen (A) k q (f∘𝐮❨n❩)
+    [ list_empty     ⇒ lift_gen (A) (λg,p. k g (𝗱(f@❨n❩)◗p)) (f∘𝐮❨n❩) q
+    | list_lcons _ _ ⇒ lift_gen (A) k (f∘𝐮❨n❩) q
     ]
-  | label_edge_L   ⇒ lift_gen (A) (λp. k (𝗟◗p)) q (⫯f)
-  | label_edge_A   ⇒ lift_gen (A) (λp. k (𝗔◗p)) q f
-  | label_edge_S   ⇒ lift_gen (A) (λp. k (𝗦◗p)) q f
+  | label_edge_L   ⇒ lift_gen (A) (λg,p. k g (𝗟◗p)) (⫯f) q
+  | label_edge_A   ⇒ lift_gen (A) (λg,p. k g (𝗔◗p)) f q
+  | label_edge_S   ⇒ lift_gen (A) (λg,p. k g (𝗦◗p)) f q
   ]
 ].
 
 interpretation
   "lift (gneric)"
-  'UpArrow A k p f = (lift_gen A k p f).
+  'UpArrow A k f p = (lift_gen A k f p).
 
-definition proj_path (p:path) (f:tr_map) ≝ p.
+definition proj_path: lift_continuation … ≝
+           λf,p.p.
 
-definition proj_rmap (p:path) (f:tr_map) ≝ f.
+definition proj_rmap: lift_continuation … ≝
+           λf,p.f.
 
 interpretation
   "lift (path)"
-  'UpArrow f p = (lift_gen ? proj_path p f).
+  'UpArrow f p = (lift_gen ? proj_path f p).
 
 interpretation
   "lift (relocation map)"
-  'UpArrow p f = (lift_gen ? proj_rmap p f).
+  'UpArrow p f = (lift_gen ? proj_rmap f p).
 
 (* Basic constructions ******************************************************)
 
 lemma lift_empty (A) (k) (f):
-      k (𝐞) f = ↑{A}❨k, 𝐞, f❩.
+      k f (𝐞) = ↑{A}❨k, f, 𝐞❩.
 // qed.
 
 lemma lift_d_empty_sn (A) (k) (n) (f):
-      ↑❨(λp. k (𝗱(f@❨n❩)◗p)), 𝐞, f∘𝐮❨ninj n❩❩ = ↑{A}❨k, 𝗱n◗𝐞, f❩.
+      ↑❨(λg,p. k g (𝗱(f@❨n❩)◗p)), f∘𝐮❨ninj n❩, 𝐞❩ = ↑{A}❨k, f, 𝗱n◗𝐞❩.
 // qed.
 
 lemma lift_d_lcons_sn (A) (k) (p) (l) (n) (f):
-      ↑❨k, l◗p, f∘𝐮❨ninj n❩❩ = ↑{A}❨k, 𝗱n◗l◗p, f❩.
+      ↑❨k, f∘𝐮❨ninj n❩, l◗p❩ = ↑{A}❨k, f, 𝗱n◗l◗p❩.
 // qed.
 
 lemma lift_L_sn (A) (k) (p) (f):
-      ↑❨(λp. k (𝗟◗p)), p, ⫯f❩ = ↑{A}❨k, 𝗟◗p, f❩.
+      ↑❨(λg,p. k g (𝗟◗p)), ⫯f, p❩ = ↑{A}❨k, f, 𝗟◗p❩.
 // qed.
 
 lemma lift_A_sn (A) (k) (p) (f):
-      ↑❨(λp. k (𝗔◗p)), p, f❩ = ↑{A}❨k, 𝗔◗p, f❩.
+      ↑❨(λg,p. k g (𝗔◗p)), f, p❩ = ↑{A}❨k, f, 𝗔◗p❩.
 // qed.
 
 lemma lift_S_sn (A) (k) (p) (f):
-      ↑❨(λp. k (𝗦◗p)), p, f❩ = ↑{A}❨k, 𝗦◗p, f❩.
+      ↑❨(λg,p. k g (𝗦◗p)), f, p❩ = ↑{A}❨k, f, 𝗦◗p❩.
 // qed.
 
 (* Basic constructions with proj_path ***************************************)
 
+lemma lift_path_empty (f):
+      (𝐞) = ↑[f]𝐞.
+// qed.
+
 lemma lift_path_d_empty_sn (f) (n):
       𝗱(f@❨n❩)◗𝐞 = ↑[f](𝗱n◗𝐞).
 // qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
index ae3ffbdc6..3413b07db 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.ma
@@ -18,7 +18,7 @@ include "ground/notation/relations/ringeq_3.ma".
 (* LIFT FOR PATH ***********************************************************)
 
 definition lift_exteq (A): relation2 (lift_continuation A) (lift_continuation A) ≝
-           λk1,k2. ∀p,f. k1 p f = k2 p f.
+           λk1,k2. ∀f,p. k1 f p = k2 f p.
 
 interpretation
   "extensional equivalence (lift continuation)"
@@ -27,7 +27,7 @@ interpretation
 (* Constructions with lift_exteq ********************************************)
 
 lemma lift_eq_repl_sn (A) (p) (k1) (k2) (f):
-      k1 ≗{A} k2 → ↑❨k1, p, f❩ = ↑❨k2, p, f❩.
+      k1 ≗{A} k2 → ↑❨k1, f, p❩ = ↑❨k2, f, p❩.
 #A #p @(path_ind_lift … p) -p [| #n | #n #l0 #q ]
 [ #k1 #k2 #f #Hk <lift_empty <lift_empty //
 |*: #IH #k1 #k2 #f #Hk /2 width=1 by/
@@ -37,13 +37,13 @@ qed-.
 (* Advanced constructions ***************************************************)
 
 lemma lift_lcons_alt (A) (k) (f) (p) (l):
-      ↑❨λp2.k(l◗p2),p,f❩ = ↑{A}❨λp2.k((l◗𝐞)●p2),p,f❩.
+      ↑❨λg,p2. k g (l◗p2), f, p❩ = ↑{A}❨λg,p2. k g ((l◗𝐞)●p2), f, p❩.
 #A #k #f #p #l
 @lift_eq_repl_sn #p2 #g // (**) (* auto fails with typechecker failure *)
 qed.
 
 lemma lift_append_rcons_sn (A) (k) (f) (p1) (p) (l):
-      ↑❨λp2.k(p1●l◗p2),p,f❩ = ↑{A}❨λp2.k(p1◖l●p2),p,f❩.
+      ↑❨λg,p2. k g (p1●l◗p2), f, p❩ = ↑{A}❨λg,p2. k g (p1◖l●p2), f, p❩.
 #A #k #f #p1 #p #l
 @lift_eq_repl_sn #p2 #g
 <list_append_rcons_sn //
@@ -52,7 +52,7 @@ qed.
 (* Advanced constructions with proj_path ************************************)
 
 lemma lift_path_append_sn (p) (f) (q):
-      q●↑[f]p = ↑❨(λp. proj_path (q●p)), p, f❩.
+      q●↑[f]p = ↑❨(λg,p. proj_path g (q●p)), f, p❩.
 #p @(path_ind_lift … p) -p // [ #n #l #p |*: #p ] #IH #f #q
 [ <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
 | <lift_L_sn <lift_L_sn >lift_lcons_alt >lift_append_rcons_sn
@@ -65,19 +65,19 @@ lemma lift_path_append_sn (p) (f) (q):
 qed.
 
 lemma lift_path_lcons (f) (p) (l):
-      l◗↑[f]p = ↑❨(λp. proj_path (l◗p)), p, f❩.
+      l◗↑[f]p = ↑❨(λg,p. proj_path g (l◗p)), f, p❩.
 #f #p #l
 >lift_lcons_alt <lift_path_append_sn //
 qed.
 
 lemma lift_path_L_sn (f) (p):
-      𝗟◗↑[⫯f]p = ↑[f](𝗟◗p).
+      (𝗟◗↑[⫯f]p) = ↑[f](𝗟◗p).
 // qed.
 
 lemma lift_path_A_sn (f) (p):
-      𝗔◗↑[f]p = ↑[f](𝗔◗p).
+      (𝗔◗↑[f]p) = ↑[f](𝗔◗p).
 // qed.
 
 lemma lift_path_S_sn (f) (p):
-      𝗦◗↑[f]p = ↑[f](𝗦◗p).
+      (𝗦◗↑[f]p) = ↑[f](𝗦◗p).
 // qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_preterm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma
similarity index 79%
rename from matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_preterm.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma
index f2c78419f..708e8a82c 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_preterm.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_prototerm.ma
@@ -12,14 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/syntax/preterm.ma".
 include "delayed_updating/substitution/lift.ma".
+include "delayed_updating/syntax/prototerm.ma".
+include "ground/lib/subset_ext_equivalence.ma".
 
-(* LIFT FOR PRETERM ***********************************************************)
-
-definition lift_preterm (f) (t): preterm ≝
-           λp. ∃∃r. r ϵ t & p = ↑[f]r.
+(* LIFT FOR PROTOTERM *******************************************************)
 
 interpretation
-  "lift (preterm)"
-  'UpArrow f t = (lift_preterm f t).
+  "lift (prototerm)"
+  'UpArrow f t = (subset_ext_f1 ? ? (lift_gen ? proj_path f) t).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
index 961a5c435..5cc0f1f48 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_structure.ma
@@ -15,6 +15,8 @@
 include "delayed_updating/substitution/lift_eq.ma".
 include "delayed_updating/syntax/path_structure.ma".
 include "delayed_updating/syntax/path_proper.ma".
+include "ground/xoa/ex_4_2.ma".
+include "ground/xoa/ex_3_2.ma".
 
 (* LIFT FOR PATH ***********************************************************)
 
@@ -31,7 +33,13 @@ lemma lift_structure (p) (f):
 #p @(path_ind_lift … p) -p //
 qed.
 
-(* Properties with proper condition for path ********************************)
+(* 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).
@@ -49,20 +57,118 @@ qed-.
 
 lemma lift_d_empty_dx (n) (p) (f):
       (⊗p)◖𝗱((↑[p]f)@❨n❩) = ↑[f](p◖𝗱n).
-/3 width=3 by ppc_lcons, lift_append_proper_dx/
+#n #p #f <lift_append_proper_dx // 
 qed.
 
 lemma lift_L_dx (p) (f):
       (⊗p)◖𝗟 = ↑[f](p◖𝗟).
-/3 width=3 by ppc_lcons, lift_append_proper_dx/
+#p #f <lift_append_proper_dx //
 qed.
 
 lemma lift_A_dx (p) (f):
       (⊗p)◖𝗔 = ↑[f](p◖𝗔).
-/3 width=3 by ppc_lcons, lift_append_proper_dx/
+#p #f <lift_append_proper_dx //
 qed.
 
 lemma lift_S_dx (p) (f):
       (⊗p)◖𝗦 = ↑[f](p◖𝗦).
-/3 width=3 by ppc_lcons, lift_append_proper_dx/
+#p #f <lift_append_proper_dx //
 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_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_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_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_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_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-.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
index 0101b8d93..ee69726db 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/bdd_term.ma
@@ -12,18 +12,18 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "delayed_updating/syntax/prototerm_constructors.ma".
+include "delayed_updating/syntax/prototerm_equivalence.ma".
+include "delayed_updating/notation/functions/class_d_phi_0.ma".
 include "ground/xoa/or_5.ma".
 include "ground/xoa/ex_3_1.ma".
 include "ground/xoa/ex_4_2.ma".
 include "ground/xoa/ex_4_3.ma".
 include "ground/xoa/ex_5_3.ma".
-include "delayed_updating/syntax/preterm_equivalence.ma".
-include "delayed_updating/syntax/preterm_constructors.ma".
-include "delayed_updating/notation/functions/class_d_phi_0.ma".
 
 (* BY-DEPTH DELAYED (BDD) TERM **********************************************)
 
-inductive bdd: 𝒫❨preterm❩ ≝
+inductive bdd: 𝒫❨prototerm❩ ≝
 | bdd_oref: ∀n. bdd (#n)
 | bdd_iref: ∀t,n. bdd t → bdd (𝛗n.t)
 | bdd_abst: ∀t. bdd t → bdd (𝛌.t)
@@ -32,7 +32,7 @@ inductive bdd: 𝒫❨preterm❩ ≝
 .
 
 interpretation
-  "by-depth delayed (preterm)"
+  "by-depth delayed (prototerm)"
   'ClassDPhi = (bdd).
 
 (* Basic inversions *********************************************************)
@@ -170,13 +170,13 @@ lemma bbd_mono_in_root_d:
 [ #t #Ht <list_cons_comm <list_cons_comm #Hn #Hl
   elim (bdd_inv_in_root_d … Ht Hn) -Ht -Hn *
   [ #H0 #_
-    lapply (preterm_root_eq_repl … H0) -H0 #H0
+    lapply (prototerm_root_eq_repl … H0) -H0 #H0
     lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
-    elim (preterm_in_root_inv_lcons_oref … Hl) -Hl //
+    elim (prototerm_in_root_inv_lcons_oref … Hl) -Hl //
   | #u #_ #_ #H0
-    lapply (preterm_root_eq_repl … H0) -H0 #H0
+    lapply (prototerm_root_eq_repl … H0) -H0 #H0
     lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
-    elim (preterm_in_root_inv_lcons_iref … Hl) -Hl //
+    elim (prototerm_in_root_inv_lcons_iref … Hl) -Hl //
   ]
 | * [ #m ] #p #IH #t #Ht
   <list_cons_shift <list_cons_shift #Hn #Hl
@@ -184,28 +184,28 @@ lemma bbd_mono_in_root_d:
     [ #_ #H0
       elim (eq_inv_list_empty_rcons ??? H0)
     | #u #Hu #Hp #H0
-      lapply (preterm_root_eq_repl … H0) -H0 #H0
+      lapply (prototerm_root_eq_repl … H0) -H0 #H0
       lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
-      elim (preterm_in_root_inv_lcons_iref … Hl) -Hl #_ #Hl
+      elim (prototerm_in_root_inv_lcons_iref … Hl) -Hl #_ #Hl
       /2 width=4 by/
     ]
   | elim (bdd_inv_in_root_L … Ht Hn) -Ht -Hn
     #u #Hu #Hp #H0
-    lapply (preterm_root_eq_repl … H0) -H0 #H0
+    lapply (prototerm_root_eq_repl … H0) -H0 #H0
     lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl  
-    elim (preterm_in_root_inv_lcons_abst … Hl) -Hl #_ #Hl
+    elim (prototerm_in_root_inv_lcons_abst … Hl) -Hl #_ #Hl
     /2 width=4 by/
   | elim (bdd_inv_in_root_A … Ht Hn) -Ht -Hn
     #v #u #_ #Hu #Hp #H0
-    lapply (preterm_root_eq_repl … H0) -H0 #H0
+    lapply (prototerm_root_eq_repl … H0) -H0 #H0
     lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
-    elim (preterm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
+    elim (prototerm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
     /2 width=4 by/
   | elim (bdd_inv_in_root_S … Ht Hn) -Ht -Hn
     #v #u #Hv #_ #Hp #H0
-    lapply (preterm_root_eq_repl … H0) -H0 #H0
+    lapply (prototerm_root_eq_repl … H0) -H0 #H0
     lapply (subset_in_eq_repl_fwd ?? … Hl … H0) -H0 -Hl #Hl
-    elim (preterm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
+    elim (prototerm_in_root_inv_lcons_appl … Hl) -Hl * #H0 #Hl destruct
     /2 width=4 by/
   ]
 ]
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma
index ed8036ba9..2d8abe304 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/path.ma
@@ -21,6 +21,7 @@ include "delayed_updating/syntax/label.ma".
 
 (* PATH *********************************************************************)
 
+(* Note: a path is a list of labels *) 
 definition path ≝ list label.
 
 interpretation
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
index 4ce090453..9da0aa838 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm.ma
@@ -12,33 +12,23 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/lib/subset.ma".
-include "delayed_updating/syntax/path.ma".
-include "delayed_updating/notation/functions/pitchfork_2.ma".
-include "delayed_updating/notation/functions/uptriangle_1.ma".
+include "delayed_updating/syntax/prototerm.ma".
+include "delayed_updating/syntax/path_structure.ma".
+include "delayed_updating/notation/relations/predicate_t_hook_1.ma".
 
 (* PRETERM ******************************************************************)
 
-(* Note: preterms are subsets of complete paths *)
-definition preterm: Type[0] ≝ 𝒫❨path❩.
+(* Note: different root paths have different structure *)
+definition structure_injective: predicate prototerm ≝
+           λt. ∀p1,p2. p1 ϵ ▵t → p2 ϵ ▵t → ⊗p1 = ⊗p2 → p1 = p2
+.
 
-definition preterm_grafted: path → preterm → preterm ≝
-           λp,t,q. p●q ϵ t.
+(* Note: a preterm is a prototerm satislying the conditions above *)
+record is_preterm (t): Prop ≝
+{
+  is_pt_injective: structure_injective t
+}.
 
 interpretation
-  "grafted (preterm)"
-  'Pitchfork t p = (preterm_grafted p t).
-
-definition preterm_root: preterm → preterm ≝
-           λt,q. ∃r. q●r ϵ t.
-
-interpretation
-  "root (preterm)"
-  'UpTriangle t = (preterm_root t).
-
-(* Basic constructions ******************************************************)
-
-lemma preterm_in_comp_root (p) (t):
-      p ϵ t → p ϵ ▵t.
-/2 width=2 by ex_intro/
-qed.
+  "preterm condition (prototerm)"
+  'PredicateTHook t = (is_preterm t).
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm.ma
new file mode 100644
index 000000000..79452e39e
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm.ma
@@ -0,0 +1,44 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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.ma".
+include "delayed_updating/syntax/path.ma".
+include "delayed_updating/notation/functions/pitchfork_2.ma".
+include "delayed_updating/notation/functions/uptriangle_1.ma".
+
+(* PROTOTERM ****************************************************************)
+
+(* Note: a prototerm is a subset of complete paths *)
+definition prototerm: Type[0] ≝ 𝒫❨path❩.
+
+definition prototerm_grafted: path → prototerm → prototerm ≝
+           λp,t,q. p●q ϵ t.
+
+interpretation
+  "grafted (prototerm)"
+  'Pitchfork t p = (prototerm_grafted p t).
+
+definition prototerm_root: prototerm → prototerm ≝
+           λt,q. ∃r. q●r ϵ t.
+
+interpretation
+  "root (prototerm)"
+  'UpTriangle t = (prototerm_root t).
+
+(* Basic constructions ******************************************************)
+
+lemma prototerm_in_comp_root (p) (t):
+      p ϵ t → p ϵ ▵t.
+/2 width=2 by ex_intro/
+qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
similarity index 73%
rename from matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
index 852fa0a59..1d3aeedf5 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_constructors.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_constructors.ma
@@ -12,44 +12,44 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "delayed_updating/syntax/preterm.ma".
+include "delayed_updating/syntax/prototerm.ma".
 include "delayed_updating/notation/functions/hash_1.ma".
 include "delayed_updating/notation/functions/phi_2.ma".
 include "delayed_updating/notation/functions/lamda_1.ma".
 include "delayed_updating/notation/functions/at_2.ma".
 
-(* CONSTRUCTORS FOR PRETERM *************************************************)
+(* CONSTRUCTORS FOR PROTOTERM ***********************************************)
 
-definition preterm_node_0 (l): preterm ≝
+definition prototerm_node_0 (l): prototerm ≝
            λp. l◗𝐞 = p.
 
-definition preterm_node_1 (l): preterm → preterm ≝
+definition prototerm_node_1 (l): prototerm → prototerm ≝
            λt,p. ∃∃q. q ϵ t & l◗q = p.
 
-definition preterm_node_2 (l1) (l2): preterm → preterm → preterm ≝
+definition prototerm_node_2 (l1) (l2): prototerm → prototerm → prototerm ≝
            λt1,t2,p.
            ∨∨ ∃∃q. q ϵ t1 & l1◗q = p
             | ∃∃q. q ϵ t2 & l2◗q = p.
 
 interpretation
-  "outer variable reference by depth (preterm)"
-  'Hash n = (preterm_node_0 (label_node_d n)).
+  "outer variable reference by depth (prototerm)"
+  'Hash n = (prototerm_node_0 (label_node_d n)).
 
 interpretation
-  "inner variable reference by depth (preterm)"
-  'Phi n t = (preterm_node_1 (label_node_d n) t).
+  "inner variable reference by depth (prototerm)"
+  'Phi n t = (prototerm_node_1 (label_node_d n) t).
 
 interpretation
-  "name-free functional abstraction (preterm)"
-  'Lamda t = (preterm_node_1 label_edge_L t).
+  "name-free functional abstraction (prototerm)"
+  'Lamda t = (prototerm_node_1 label_edge_L t).
 
 interpretation
-  "application (preterm)"
-  'At u t = (preterm_node_2 label_edge_S label_edge_A u t).
+  "application (prototerm)"
+  'At u t = (prototerm_node_2 label_edge_S label_edge_A u t).
 
 (* Basic Inversions *********************************************************)
 
-lemma preterm_in_root_inv_lcons_oref:
+lemma prototerm_in_root_inv_lcons_oref:
       ∀p,l,n. l◗p ϵ ▵#n →
       ∧∧ 𝗱n = l & 𝐞 = p.
 #p #l #n * #q
@@ -58,7 +58,7 @@ elim (eq_inv_list_empty_append … e0) -e0 #H0 #_
 /2 width=1 by conj/
 qed-.
 
-lemma preterm_in_root_inv_lcons_iref:
+lemma prototerm_in_root_inv_lcons_iref:
       ∀t,p,l,n. l◗p ϵ ▵𝛗n.t →
       ∧∧ 𝗱n = l & p ϵ ▵t.
 #t #p #l #n * #q
@@ -66,7 +66,7 @@ lemma preterm_in_root_inv_lcons_iref:
 /3 width=2 by ex_intro, conj/
 qed-.
 
-lemma preterm_in_root_inv_lcons_abst:
+lemma prototerm_in_root_inv_lcons_abst:
       ∀t,p,l. l◗p ϵ ▵𝛌.t →
       ∧∧ 𝗟 = l & p ϵ ▵t.
 #t #p #l * #q
@@ -74,7 +74,7 @@ lemma preterm_in_root_inv_lcons_abst:
 /3 width=2 by ex_intro, conj/
 qed-.
 
-lemma preterm_in_root_inv_lcons_appl:
+lemma prototerm_in_root_inv_lcons_appl:
       ∀u,t,p,l. l◗p ϵ ▵@u.t →
       ∨∨ ∧∧ 𝗦 = l & p ϵ ▵u
        | ∧∧ 𝗔 = l & p ϵ ▵t.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_equivalence.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_equivalence.ma
similarity index 81%
rename from matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_equivalence.ma
rename to matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_equivalence.ma
index 6f788a7a6..414c47d27 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/preterm_equivalence.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_equivalence.ma
@@ -13,20 +13,20 @@
 (**************************************************************************)
 
 include "ground/lib/subset_equivalence.ma".
-include "delayed_updating/syntax/preterm.ma".
+include "delayed_updating/syntax/prototerm.ma".
 
-(* EQUIVALENCE FOR PRETERM **************************************************)
+(* EQUIVALENCE FOR PROTOTERM ************************************************)
 
-(* Constructions with preterm_root ******************************************)
+(* Constructions with prototerm_root ****************************************)
 
-lemma preterm_root_incl_repl:
+lemma prototerm_root_incl_repl:
       ∀t1,t2. t1 ⊆ t2 → ▵t1 ⊆ ▵t2.
 #t1 #t2 #Ht #p * #q #Hq
 /3 width=2 by ex_intro/
 qed.
 
-lemma preterm_root_eq_repl:
+lemma prototerm_root_eq_repl:
       ∀t1,t2. t1 ⇔ t2 → ▵t1 ⇔ ▵t2.
 #t1 #t2 * #H1 #H2
-/3 width=3 by conj, preterm_root_incl_repl/
+/3 width=3 by conj, prototerm_root_incl_repl/
 qed.
diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper.ma b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper.ma
new file mode 100644
index 000000000..9a5569726
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/syntax/prototerm_proper.ma
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "delayed_updating/syntax/path_proper.ma".
+include "ground/lib/subset_ext_equivalence.ma".
+
+(* PROPER CONDITION FOR PROTOTERM *******************************************)
+
+interpretation
+  "proper condition (prototerm)"
+  'PredicatePTail t = (subset_ext_p1 path ppc t).
+
+(* Basic constructions ******************************************************)
+
+lemma tpc_i (t):
+      (𝐞 ⧸ϵ t) → Ꝕt.
+#t #Ht * //
+#H elim (Ht H)
+qed.
+
+(* Basic inversions *********************************************************)
+
+lemma tpc_e (t): Ꝕt → 𝐞 ϵ t → ⊥.
+/2 width=5 by subset_in_inv_ext_p1_dx/ qed-.
-- 
2.39.2