From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 13 Jan 2013 19:10:32 +0000 (+0000)
Subject: standardization: equivalence between paths and left residuals started
X-Git-Tag: make_still_working~1356
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=04cca085e96987e43b58f001bc8af317eb427ff2;p=helm.git

standardization: equivalence between paths and left residuals started
---

diff --git a/matita/matita/contribs/lambda/background/notation.ma b/matita/matita/contribs/lambda/background/notation.ma
index c698a5b12..62b8b2dca 100644
--- a/matita/matita/contribs/lambda/background/notation.ma
+++ b/matita/matita/contribs/lambda/background/notation.ma
@@ -14,6 +14,16 @@
 
 (* GENERIC NOTATION *********************************************************)
 
+(* Note: this should go to core_notation *)
+notation "⊥"
+  non associative with precedence 90
+  for @{'false}.
+
+(* Note: this should go to core_notation *)
+notation "⊤"
+  non associative with precedence 90
+  for @{'true}.
+
 (* Note: this should go to core_notation *)
 notation "hvbox(a break ≺ b)"
    non associative with precedence 45
diff --git a/matita/matita/contribs/lambda/background/preamble.ma b/matita/matita/contribs/lambda/background/preamble.ma
index dc5c14467..31efafd7e 100644
--- a/matita/matita/contribs/lambda/background/preamble.ma
+++ b/matita/matita/contribs/lambda/background/preamble.ma
@@ -18,15 +18,20 @@ include "arithmetics/exp.ma".
 
 include "background/xoa_notation.ma".
 include "background/xoa.ma".
+include "background/notation.ma".
 
 (* logic *)
 
 (* Note: For some reason this cannot be in the standard library *) 
 interpretation "logical false" 'false = False.
 
-notation "⊥"
-  non associative with precedence 90
-  for @{'false}.
+(* booleans *)
+
+(* Note: For some reason this cannot be in the standard library *) 
+interpretation "boolean false" 'false = false.
+
+(* Note: For some reason this cannot be in the standard library *) 
+interpretation "boolean true" 'true = true.
 
 (* arithmetics *)
 
diff --git a/matita/matita/contribs/lambda/background/xoa.ma b/matita/matita/contribs/lambda/background/xoa.ma
index 5f029c5fc..f18b06ec9 100644
--- a/matita/matita/contribs/lambda/background/xoa.ma
+++ b/matita/matita/contribs/lambda/background/xoa.ma
@@ -32,6 +32,14 @@ inductive ex2_3 (A0,A1,A2:Type[0]) (P0,P1:A0→A1→A2→Prop) : Prop ≝
 
 interpretation "multiple existental quantifier (2, 3)" 'Ex P0 P1 = (ex2_3 ? ? ? P0 P1).
 
+(* multiple existental quantifier (3, 1) *)
+
+inductive ex3 (A0:Type[0]) (P0,P1,P2:A0→Prop) : Prop ≝
+   | ex3_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → ex3 ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (3, 1)" 'Ex P0 P1 P2 = (ex3 ? P0 P1 P2).
+
 (* multiple existental quantifier (3, 2) *)
 
 inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝
@@ -48,6 +56,30 @@ inductive ex3_3 (A0,A1,A2:Type[0]) (P0,P1,P2:A0→A1→A2→Prop) : Prop ≝
 
 interpretation "multiple existental quantifier (3, 3)" 'Ex P0 P1 P2 = (ex3_3 ? ? ? P0 P1 P2).
 
+(* multiple existental quantifier (3, 4) *)
+
+inductive ex3_4 (A0,A1,A2,A3:Type[0]) (P0,P1,P2:A0→A1→A2→A3→Prop) : Prop ≝
+   | ex3_4_intro: ∀x0,x1,x2,x3. P0 x0 x1 x2 x3 → P1 x0 x1 x2 x3 → P2 x0 x1 x2 x3 → ex3_4 ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (3, 4)" 'Ex P0 P1 P2 = (ex3_4 ? ? ? ? P0 P1 P2).
+
+(* multiple existental quantifier (4, 1) *)
+
+inductive ex4 (A0:Type[0]) (P0,P1,P2,P3:A0→Prop) : Prop ≝
+   | ex4_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → P3 x0 → ex4 ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (4, 1)" 'Ex P0 P1 P2 P3 = (ex4 ? P0 P1 P2 P3).
+
+(* multiple existental quantifier (4, 2) *)
+
+inductive ex4_2 (A0,A1:Type[0]) (P0,P1,P2,P3:A0→A1→Prop) : Prop ≝
+   | ex4_2_intro: ∀x0,x1. P0 x0 x1 → P1 x0 x1 → P2 x0 x1 → P3 x0 x1 → ex4_2 ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (4, 2)" 'Ex P0 P1 P2 P3 = (ex4_2 ? ? P0 P1 P2 P3).
+
 (* multiple existental quantifier (4, 3) *)
 
 inductive ex4_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3:A0→A1→A2→Prop) : Prop ≝
diff --git a/matita/matita/contribs/lambda/background/xoa_notation.ma b/matita/matita/contribs/lambda/background/xoa_notation.ma
index a978cb1b7..37443443b 100644
--- a/matita/matita/contribs/lambda/background/xoa_notation.ma
+++ b/matita/matita/contribs/lambda/background/xoa_notation.ma
@@ -34,6 +34,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) }.
 
+(* multiple existental quantifier (3, 1) *)
+
+notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) }.
+
+notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) }.
+
 (* multiple existental quantifier (3, 2) *)
 
 notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
@@ -54,6 +64,36 @@ notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break
  non associative with precedence 20
  for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) }.
 
+(* multiple existental quantifier (3, 4) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.λ${ident x3}.$P2) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 , ident x3 break . term 19 P0 break & term 19 P1 break & term 19 P2)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.λ${ident x3}:$T3.$P2) }.
+
+(* multiple existental quantifier (4, 1) *)
+
+notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) (λ${ident x0}.$P3) }.
+
+notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) (λ${ident x0}:$T0.$P3) }.
+
+(* multiple existental quantifier (4, 2) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.λ${ident x1}.$P0) (λ${ident x0}.λ${ident x1}.$P1) (λ${ident x0}.λ${ident x1}.$P2) (λ${ident x0}.λ${ident x1}.$P3) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P3) }.
+
 (* multiple existental quantifier (4, 3) *)
 
 notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3)"
diff --git a/matita/matita/contribs/lambda/paths/dst_computation.ma b/matita/matita/contribs/lambda/paths/dst_computation.ma
index 2e5310a11..f7740daf7 100644
--- a/matita/matita/contribs/lambda/paths/dst_computation.ma
+++ b/matita/matita/contribs/lambda/paths/dst_computation.ma
@@ -27,11 +27,11 @@ inductive dst: relation term ≝
 .
 
 interpretation "decomposed standard computation"
-    'Std M N = (dst M N).
+    'DecomposedStd M N = (dst M N).
 
 notation "hvbox( M break ⓢ↦* term 46 N )"
    non associative with precedence 45
-   for @{ 'Std $M $N }.
+   for @{ 'DecomposedStd $M $N }.
 
 lemma dst_inv_lref: ∀M,N. M ⓢ↦* N → ∀j. #j = N →
                     ∃∃s. is_whd s & M ↦*[s] #j.
diff --git a/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma b/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma
new file mode 100644
index 000000000..253f2ae73
--- /dev/null
+++ b/matita/matita/contribs/lambda/paths/labeled_st_reduction.ma
@@ -0,0 +1,197 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "subterms/delifting_substitution.ma".
+include "subterms/projections.ma".
+include "paths/standard_order.ma".
+
+(* PATH-LABELED STANDARD REDUCTION ON SUBTERMS (SINGLE STEP) ****************)
+
+(* Note: this is standard reduction on marked redexes,
+         left residuals are unmarked in the reductum
+*)
+inductive pl_st: path → relation subterms ≝
+| pl_st_beta   : ∀V,T. pl_st (◊) ({⊤}@V.{⊤}𝛌.T) ([↙V]T)
+| pl_st_abst   : ∀b,p,T1,T2. pl_st p T1 T2 → pl_st (rc::p) ({b}𝛌.T1) ({⊥}𝛌.T2) 
+| pl_st_appl_sn: ∀b,p,V1,V2,T. pl_st p V1 V2 → pl_st (sn::p) ({b}@V1.T) ({⊥}@V2.{⊥}⇕T)
+| pl_st_appl_dx: ∀b,p,V,T1,T2. pl_st p T1 T2 → pl_st (dx::p) ({b}@V.T1) ({b}@V.T2)
+.
+
+interpretation "path-labeled standard reduction"
+    'Std F p G = (pl_st p F G).
+
+notation "hvbox( F break Ⓡ ↦ [ term 46 p ] break term 46 G )"
+   non associative with precedence 45
+   for @{ 'Std $F $p $G }.
+(*
+lemma pl_st_inv_pl_sred: ∀p,F,G. F Ⓡ↦[p] G → ⇓F ↦[p] ⇓G.
+#p #F #G #H elim H -p -F -G // /2 width=1/
+qed-.
+
+lemma pl_st_inv_vref: ∀p,F,G. F Ⓡ↦[p] G → ∀b,i. {b}#i = F → ⊥.
+/3 width=5 by pl_st_inv_st, st_inv_vref/
+qed-.
+*)
+lemma pl_st_inv_abst: ∀p,F,G. F Ⓡ↦[p] G → ∀b0,U1. {b0}𝛌.U1 = F →
+                      ∃∃q,U2. U1 Ⓡ↦[q] U2 & rc::q = p & {⊥}𝛌.U2 = G.
+#p #F #G * -p -F -G
+[ #V #T #b0 #U1 #H destruct
+| #b #p #T1 #T2 #HT12 #b0 #U1 #H destruct /2 width=5/
+| #b #p #V1 #V2 #T #_ #b0 #U1 #H destruct
+| #b #p #V #T1 #T2 #_ #b0 #U1 #H destruct
+]
+qed-.
+
+lemma pl_st_inv_appl: ∀p,F,G. F Ⓡ↦[p] G → ∀b0,W,U. {b0}@W.U = F →
+                      ∨∨ (∃∃U0. ⊤ = b0 & ◊ = p & {⊤}𝛌.U0 = U & [↙W] U0 = G)
+                       | (∃∃q,W0. sn::q = p & W Ⓡ↦[q] W0 & {⊥}@W0.{⊥}⇕U = G)
+                       | (∃∃q,U0. dx::q = p & U Ⓡ↦[q] U0 & {b0}@W.U0 = G).
+#p #F #G * -p -F -G
+[ #V #T #b0 #W #U #H destruct /3 width=3/
+| #b #p #T1 #T2 #_ #b0 #W #U #H destruct
+| #b #p #V1 #V2 #T #HV12 #b0 #W #U #H destruct /3 width=5/
+| #b #p #V #T1 #T2 #HT12 #b0 #W #U #H destruct /3 width=5/
+]
+qed-.
+
+lemma pl_st_fwd_abst: ∀p,F,G. F Ⓡ↦[p] G → ∀b0,U2. {b0}𝛌.U2 = G →
+                      ◊ = p ∨ ∃q. rc::q = p.
+#p #F #G * -p -F -G
+[ /2 width=1/
+| /3 width=2/
+| #b #p #V1 #V2 #T #_ #b0 #U2 #H destruct
+| #b #p #V #T1 #T2 #_ #b0 #U2 #H destruct
+]
+qed-.
+
+lemma pl_st_inv_nil: ∀p,F,G. F Ⓡ↦[p] G → ◊ = p →
+                     ∃∃V,T. {⊤}@V.{⊤} 𝛌.T = F & [↙V] T = G.
+#p #F #G * -p -F -G
+[ #V #T #_ destruct /2 width=4/
+| #b #p #T1 #T2 #_ #H destruct
+| #b #p #V1 #V2 #T #_ #H destruct
+| #b #p #V #T1 #T2 #_ #H destruct
+]
+qed-.
+
+lemma pl_st_inv_rc: ∀p,F,G. F Ⓡ↦[p] G → ∀q. rc::q = p →
+                    ∃∃b,T1,T2. T1 Ⓡ↦[q] T2 & {b}𝛌.T1 = F & {⊥}𝛌.T2 = G.
+#p #F #G * -p -F -G
+[ #V #T #q #H destruct
+| #b #p #T1 #T2 #HT12 #q #H destruct /2 width=6/
+| #b #p #V1 #V2 #T #_ #q #H destruct
+| #b #p #V #T1 #T2 #_ #q #H destruct
+]
+qed-.
+
+lemma pl_st_inv_sn: ∀p,F,G. F Ⓡ↦[p] G → ∀q. sn::q = p →
+                    ∃∃b,V1,V2,T. V1 Ⓡ↦[q] V2 & {b}@V1.T = F & {⊥}@V2.{⊥}⇕T = G.
+#p #F #G * -p -F -G
+[ #V #T #q #H destruct
+| #b #p #T1 #T2 #_ #q #H destruct
+| #b #p #V1 #V2 #T #HV12 #q #H destruct /2 width=7/
+| #b #p #V #T1 #T2 #_ #q #H destruct
+]
+qed-.
+
+lemma pl_st_inv_dx: ∀p,F,G. F Ⓡ↦[p] G → ∀q. dx::q = p →
+                    ∃∃b,V,T1,T2. T1 Ⓡ↦[q] T2 & {b}@V.T1 = F & {b}@V.T2 = G.
+#p #F #G * -p -F -G
+[ #V #T #q #H destruct
+| #b #p #T1 #T2 #_ #q #H destruct
+| #b #p #V1 #V2 #T #_ #q #H destruct
+| #b #p #V #T1 #T2 #HT12 #q #H destruct /2 width=7/
+]
+qed-.
+
+
+
+(*
+lemma pl_st_lift: ∀p. sliftable (pl_st p).
+#p #h #F1 #F2 #H elim H -p -F1 -F2 normalize /2 width=1/
+[ #V #T #d <sdsubst_slift_le //
+| #b #p #V1 #V2 #T #_ #IHV12 #d
+qed.
+
+lemma pl_st_inv_lift: ∀p. deliftable_sn (pl_st p).
+#p #h #G1 #G2 #H elim H -p -G1 -G2
+[ #W #U #d #F1 #H
+  elim (lift_inv_appl … H) -H #V #F #H0 #HF #H destruct
+  elim (lift_inv_abst … HF) -HF #T #H0 #H destruct /3 width=3/
+| #p #U1 #U2 #_ #IHU12 #d #F1 #H
+  elim (lift_inv_abst … H) -H #T1 #HTU1 #H
+  elim (IHU12 … HTU1) -U1 #T2 #HT12 #HTU2 destruct
+  @(ex2_intro … (𝛌.T2)) // /2 width=1/
+| #p #W1 #W2 #U1 #_ #IHW12 #d #F1 #H
+  elim (lift_inv_appl … H) -H #V1 #T #HVW1 #H1 #H2
+  elim (IHW12 … HVW1) -W1 #V2 #HV12 #HVW2 destruct
+  @(ex2_intro … (@V2.T)) // /2 width=1/
+| #p #W1 #U1 #U2 #_ #IHU12 #d #F1 #H
+  elim (lift_inv_appl … H) -H #V #T1 #H1 #HTU1 #H2
+  elim (IHU12 … HTU1) -U1 #T2 #HT12 #HTU2 destruct
+  @(ex2_intro … (@V.T2)) // /2 width=1/
+]
+qed-.
+
+lemma pl_st_dsubst: ∀p. sdsubstable_dx (pl_st p).
+#p #W1 #F1 #F2 #H elim H -p -F1 -F2 normalize /2 width=1/
+#W2 #T #d >dsubst_dsubst_ge //
+qed.
+*)
+
+lemma pl_st_inv_empty: ∀p,G1,G2. G1 Ⓡ↦[p] G2 → ∀F1. {⊥}⇕F1 = G1 → ⊥.
+#p #F1 #F2 #H elim H -p -F1 -F2
+[ #V #T #F1 #H
+  elim (mk_boolean_inv_appl … H) -H #b0 #W #U #H destruct
+| #b #p #T1 #T2 #_ #IHT12 #F1 #H
+  elim (mk_boolean_inv_abst … H) -H /2 width=2/
+| #b #p #V1 #V2 #T #_ #IHV12 #F1 #H
+  elim (mk_boolean_inv_appl … H) -H /2 width=2/
+| #b #p #V #T1 #T2 #_ #IHT12 #F1 #H
+  elim (mk_boolean_inv_appl … H) -H /2 width=2/
+]
+qed-.
+
+theorem pl_st_mono: ∀p. singlevalued … (pl_st p).
+#p #F #G1 #H elim H -p -F -G1
+[ #V #T #G2 #H elim (pl_st_inv_nil … H ?) -H //
+  #W #U #H #HG2 destruct //
+| #b #p #T1 #T2 #_ #IHT12 #G2 #H elim (pl_st_inv_rc … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+  #b0 #U1 #U2 #HU12 #H #HG2 destruct /3 width=1/
+| #b #p #V1 #V2 #T #_ #IHV12 #G2 #H elim (pl_st_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+  #b0 #W1 #W2 #U #HW12 #H #HG2 destruct /3 width=1/
+| #b #p #V #T1 #T2 #_ #IHT12 #G2 #H elim (pl_st_inv_dx … H ??) -H [3: // |2: skip ] (**) (* simplify line *)
+  #b0 #W #U1 #U2 #HU12 #H #HG2 destruct /3 width=1/
+]
+qed-.
+
+theorem pl_st_inv_is_standard: ∀p1,F1,F. F1 Ⓡ↦[p1] F →
+                               ∀p2,F2. F Ⓡ↦[p2] F2 → p1 ≤ p2.
+#p1 #F1 #F #H elim H -p1 -F1 -F //
+[ #b #p #T1 #T #_ #IHT1 #p2 #F2 #H elim (pl_st_inv_abst … H ???) -H [3: // |2,4: skip ] (**) (* simplify line *)
+  #q #T2 #HT2 #H1 #H2 destruct /3 width=2/
+| #b #p #V1 #V #T #_ #IHV1 #p2 #F2 #H elim (pl_st_inv_appl … H ????) -H [7: // |2,3,4: skip ] * (**) (* simplify line *)
+  [ #U #H destruct
+  | #q #V2 #H1 #HV2 #H2 destruct /3 width=2/
+  | #q #U #_ #H elim (pl_st_inv_empty … H ??) [ // | skip ] (**) (* simplify line *)
+  ]
+| #b #p #V #T1 #T #HT1 #IHT1 #p2 #F2 #H elim (pl_st_inv_appl … H ????) -H [7: // |2,3,4: skip ] * (**) (* simplify line *)
+  [ #U #_ #H1 #H2 #_ -b -V -F2 -IHT1
+    elim (pl_st_fwd_abst … HT1 … H2) // -H1 * #q #H
+    elim (pl_st_inv_rc … HT1 … H) -HT1 -H #b #U1 #U2 #_ #_ #H -b -q -T1 -U1 destruct
+  | #q #V2 #H1 #_ #_ -b -F2 -T1 -T -V -V2 destruct //
+  | #q #T2 #H1 #HT2 #H2 -b -F2 -T1 -V /3 width=2/
+  ]
+]
+qed-.
diff --git a/matita/matita/contribs/lambda/subterms/delifting_substitution.ma b/matita/matita/contribs/lambda/subterms/delifting_substitution.ma
new file mode 100644
index 000000000..272c75460
--- /dev/null
+++ b/matita/matita/contribs/lambda/subterms/delifting_substitution.ma
@@ -0,0 +1,155 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "subterms/lift.ma".
+
+(* DELIFTING SUBSTITUTION ***************************************************)
+
+(* Policy: depth (level) metavariables: d, e (as for lift) *)
+let rec sdsubst G d F on F ≝ match F with
+[ SVRef b i   ⇒ tri … i d ({b}#i) (↑[i] G) ({b}#(i-1))
+| SAbst b T   ⇒ {b}𝛌. (sdsubst G (d+1) T)
+| SAppl b V T ⇒ {b}@ (sdsubst G d V). (sdsubst G d T)
+].
+
+interpretation "delifting substitution for subterms"
+   'DSubst G d F = (sdsubst G d F).
+
+lemma sdsubst_vref_lt: ∀b,i,d,G. i < d → [d ↙ G] {b}#i = {b}#i.
+normalize /2 width=1/
+qed.
+
+lemma sdsubst_vref_eq: ∀b,i,G. [i ↙ G] {b}#i = ↑[i]G.
+normalize //
+qed.
+
+lemma sdsubst_vref_gt: ∀b,i,d,G. d < i → [d ↙ G] {b}#i = {b}#(i-1).
+normalize /2 width=1/
+qed.
+
+theorem sdsubst_slift_le: ∀h,G,F,d1,d2. d2 ≤ d1 →
+                          [d2 ↙ ↑[d1 - d2, h] G] ↑[d1 + 1, h] F = ↑[d1, h] [d2 ↙ G] F.
+#h #G #F elim F -F
+[ #b #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2
+  [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
+    >(sdsubst_vref_lt … Hid2) >(slift_vref_lt … Hid1) >slift_vref_lt /2 width=1/
+  | destruct >sdsubst_vref_eq >slift_vref_lt /2 width=1/
+  | >(sdsubst_vref_gt … Hid2) -Hd21 elim (lt_or_ge (i-1) d1) #Hi1d1
+    [ >(slift_vref_lt … Hi1d1) >slift_vref_lt /2 width=1/
+    | lapply (ltn_to_ltO … Hid2) #Hi
+      >(slift_vref_ge … Hi1d1) >slift_vref_ge /2 width=1/ -Hi1d1 >plus_minus // /3 width=1/
+    ]
+  ]
+| normalize #b #T #IHT #d1 #d2 #Hd21
+  lapply (IHT (d1+1) (d2+1) ?) -IHT /2 width=1/
+| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd21
+  >IHV -IHV // >IHT -IHT //
+]
+qed.
+
+theorem sdsubst_slift_be: ∀h,G,F,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
+                          [d2 ↙ G] ↑[d1, h + 1] F = ↑[d1, h] F.
+#h #G #F elim F -F
+[ #b #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
+  [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
+    >(slift_vref_lt … Hid1) >(slift_vref_lt … Hid1) /2 width=1/
+  | lapply (transitive_le … (i+h) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
+    >(slift_vref_ge … Hid1) >(slift_vref_ge … Hid1) -Hid1
+    >sdsubst_vref_gt // /2 width=1/
+  ]
+| normalize #b #T #IHT #d1 #d2 #Hd12 #Hd21
+  >IHT -IHT // /2 width=1/
+| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12 #Hd21
+  >IHV -IHV // >IHT -IHT //
+]
+qed.
+
+theorem sdsubst_slift_ge: ∀h,G,F,d1,d2. d1 + h ≤ d2 →
+                          [d2 ↙ G] ↑[d1, h] F = ↑[d1, h] [d2 - h ↙ G] F.
+#h #G #F elim F -F
+[ #b #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h
+  [ >(sdsubst_vref_lt … Hid2h) elim (lt_or_ge i d1) #Hid1
+    [ lapply (lt_to_le_to_lt … (d1+h) Hid1 ?) -Hid2h // #Hid1h
+      lapply (lt_to_le_to_lt … Hid1h Hd12) -Hid1h -Hd12 #Hid2
+      >(slift_vref_lt … Hid1) -Hid1 /2 width=1/
+    | >(slift_vref_ge … Hid1) -Hid1 -Hd12 /3 width=1/
+    ]
+  | destruct elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hhd2
+    >sdsubst_vref_eq >slift_vref_ge // >slift_slift_be // <plus_minus_m_m //
+  | elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #_
+    lapply (le_to_lt_to_lt … Hd12 Hid2h) -Hd12 #Hid1
+    lapply (ltn_to_ltO … Hid2h) #Hi
+    >(sdsubst_vref_gt … Hid2h)
+    >slift_vref_ge /2 width=1/ >slift_vref_ge /2 width=1/ -Hid1
+    >sdsubst_vref_gt /2 width=1/ -Hid2h >plus_minus //
+  ]
+| normalize #b #T #IHT #d1 #d2 #Hd12
+  elim (le_inv_plus_l … Hd12) #_ #Hhd2
+  >IHT -IHT /2 width=1/ <plus_minus //
+| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12
+  >IHV -IHV // >IHT -IHT //
+]
+qed.
+
+theorem sdsubst_sdsubst_ge: ∀G1,G2,F,d1,d2. d1 ≤ d2 →
+                            [d2 ↙ G2] [d1 ↙ G1] F = [d1 ↙ [d2 - d1 ↙ G2] G1] [d2 + 1 ↙ G2] F.
+#G1 #G2 #F elim F -F
+[ #b #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1
+  [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2
+    >(sdsubst_vref_lt … Hid1) >(sdsubst_vref_lt … Hid2) >sdsubst_vref_lt /2 width=1/
+  | destruct >sdsubst_vref_eq >sdsubst_vref_lt /2 width=1/
+  | >(sdsubst_vref_gt … Hid1) elim (lt_or_eq_or_gt i (d2+1)) #Hid2
+    [ lapply (ltn_to_ltO … Hid1) #Hi
+      >(sdsubst_vref_lt … Hid2) >sdsubst_vref_lt /2 width=1/
+    | destruct /2 width=1/
+    | lapply (le_to_lt_to_lt (d1+1) … Hid2) -Hid1 /2 width=1/ -Hd12 #Hid1
+      >(sdsubst_vref_gt … Hid2) >sdsubst_vref_gt /2 width=1/
+      >sdsubst_vref_gt // /2 width=1/
+    ]
+  ]
+| normalize #b #T #IHT #d1 #d2 #Hd12
+  lapply (IHT (d1+1) (d2+1) ?) -IHT /2 width=1/
+| normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12
+  >IHV -IHV // >IHT -IHT //
+]
+qed.
+
+theorem sdsubst_sdsubst_lt: ∀G1,G2,F,d1,d2. d2 < d1 →
+                            [d2 ↙ [d1 - d2 -1 ↙ G1] G2] [d1 ↙ G1] F = [d1 - 1 ↙ G1] [d2 ↙ G2] F.
+#G1 #G2 #F #d1 #d2 #Hd21
+lapply (ltn_to_ltO … Hd21) #Hd1
+>sdsubst_sdsubst_ge in ⊢ (???%); /2 width=1/ <plus_minus_m_m //
+qed.
+
+definition sdsubstable_dx: predicate (relation subterms) ≝ λR.
+                           ∀G,F1,F2. R F1 F2 → ∀d. R ([d ↙ G] F1) ([d ↙ G] F2).
+(*
+definition sdsubstable: predicate (relation subterms) ≝ λR.
+                        ∀G1,G2. R G1 G2 → ∀F1,F2. R F1 F2 → ∀d. R ([d ↙ G1] F1) ([d ↙ G2] F2).
+
+lemma star_sdsubstable_dx: ∀R. sdsubstable_dx R → sdsubstable_dx (star … R).
+#R #HR #G #F1 #F2 #H elim H -F2 // /3 width=3/
+qed.
+
+lemma lstar_sdsubstable_dx: ∀S,R. (∀a. sdsubstable_dx (R a)) →
+                            ∀l. sdsubstable_dx (lstar S … R l).
+#S #R #HR #l #G #F1 #F2 #H
+@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/
+qed.
+
+lemma star_sdsubstable: ∀R. reflexive ? R →
+                        sdsubstable R → sdsubstable (star … R).
+#R #H1R #H2 #G1 #G2 #H elim H -G2 /3 width=1/ /3 width=5/
+qed.
+*)
diff --git a/matita/matita/contribs/lambda/subterms/lift.ma b/matita/matita/contribs/lambda/subterms/lift.ma
index c86695ffb..0917949f0 100644
--- a/matita/matita/contribs/lambda/subterms/lift.ma
+++ b/matita/matita/contribs/lambda/subterms/lift.ma
@@ -218,37 +218,37 @@ elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hh1d2
 lapply (sym_eq subterms … H) -H >(plus_minus_m_m … Hh1d2) in ⊢ (???%→?); -Hh1d2 #H
 elim (slift_inv_slift_le … Hd12 … H) -H -Hd12 /2 width=3/
 qed-.
-(*
-definition liftable: predicate (relation term) ≝ λR.
-                     ∀h,M1,M2. R M1 M2 → ∀d. R (↑[d, h] M1) (↑[d, h] M2).
 
-definition deliftable_sn: predicate (relation term) ≝ λR.
-                          ∀h,N1,N2. R N1 N2 → ∀d,M1. ↑[d, h] M1 = N1 →
-                          ∃∃M2. R M1 M2 & ↑[d, h] M2 = N2.
+definition sliftable: predicate (relation subterms) ≝ λR.
+                      ∀h,F1,F2. R F1 F2 → ∀d. R (↑[d, h] F1) (↑[d, h] F2).
 
-lemma star_liftable: ∀R. liftable R → liftable (star … R).
-#R #HR #h #M1 #M2 #H elim H -M2 // /3 width=3/
+definition sdeliftable_sn: predicate (relation subterms) ≝ λR.
+                           ∀h,G1,G2. R G1 G2 → ∀d,F1. ↑[d, h] F1 = G1 →
+                           ∃∃F2. R F1 F2 & ↑[d, h] F2 = G2.
+(*
+lemma star_sliftable: ∀R. sliftable R → sliftable (star … R).
+#R #HR #h #F1 #F2 #H elim H -F2 // /3 width=3/
 qed.
 
-lemma star_deliftable_sn: ∀R. deliftable_sn R → deliftable_sn (star … R).
-#R #HR #h #N1 #N2 #H elim H -N2 /2 width=3/
-#N #N2 #_ #HN2 #IHN1 #d #M1 #HMN1
-elim (IHN1 … HMN1) -N1 #M #HM1 #HMN
-elim (HR … HN2 … HMN) -N /3 width=3/
+lemma star_deliftable_sn: ∀R. sdeliftable_sn R → sdeliftable_sn (star … R).
+#R #HR #h #G1 #G2 #H elim H -G2 /2 width=3/
+#G #G2 #_ #HG2 #IHG1 #d #F1 #HFG1
+elim (IHG1 … HFG1) -G1 #F #HF1 #HFG
+elim (HR … HG2 … HFG) -G /3 width=3/
 qed-.
 
-lemma lstar_liftable: ∀S,R. (∀a. liftable (R a)) →
-                      ∀l. liftable (lstar S … R l).
-#S #R #HR #l #h #M1 #M2 #H
-@(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
+lemma lstar_sliftable: ∀S,R. (∀a. sliftable (R a)) →
+                       ∀l. sliftable (lstar S … R l).
+#S #R #HR #l #h #F1 #F2 #H
+@(lstar_ind_l ????????? H) -l -F1 // /3 width=3/
 qed.
 
-lemma lstar_deliftable_sn: ∀S,R. (∀a. deliftable_sn (R a)) →
-                           ∀l. deliftable_sn (lstar S … R l).
-#S #R #HR #l #h #N1 #N2 #H
-@(lstar_ind_l ????????? H) -l -N1 /2 width=3/
-#a #l #N1 #N #HN1 #_ #IHN2 #d #M1 #HMN1
-elim (HR … HN1 … HMN1) -N1 #M #HM1 #HMN
-elim (IHN2 … HMN) -N /3 width=3/
+lemma lstar_sdeliftable_sn: ∀S,R. (∀a. sdeliftable_sn (R a)) →
+                            ∀l. sdeliftable_sn (lstar S … R l).
+#S #R #HR #l #h #G1 #G2 #H
+@(lstar_ind_l ????????? H) -l -G1 /2 width=3/
+#a #l #G1 #G #HG1 #_ #IHG2 #d #F1 #HFG1
+elim (HR … HG1 … HFG1) -G1 #F #HF1 #HFG
+elim (IHG2 … HFG) -G /3 width=3/
 qed-.
 *)
diff --git a/matita/matita/contribs/lambda/subterms/projections.ma b/matita/matita/contribs/lambda/subterms/projections.ma
new file mode 100644
index 000000000..026a359c9
--- /dev/null
+++ b/matita/matita/contribs/lambda/subterms/projections.ma
@@ -0,0 +1,128 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "terms/term.ma".
+include "subterms/subterms.ma".
+
+(* PROJECTIONS **************************************************************)
+
+(* Note: the boolean subset of subterms *) 
+let rec boolean b M on M ≝ match M with
+[ VRef i   ⇒ {b}#i
+| Abst A   ⇒ {b}𝛌.(boolean b A)
+| Appl B A ⇒ {b}@(boolean b B).(boolean b A)
+].
+
+interpretation "boolean subset (subterms)"
+   'ProjectUp b M = (boolean b M).
+
+notation "hvbox( { term 46 b } ⇑ break term 46 M)"
+   non associative with precedence 46
+   for @{ 'ProjectUp $b $M }.
+
+lemma boolean_inv_vref: ∀j,b0,b,M. {b}⇑ M = {b0}#j → b = b0 ∧ M = #j.
+#j #b0 #b * normalize
+[ #i #H destruct /2 width=1/
+| #A #H destruct
+| #B #A #H destruct
+]
+qed-.
+
+lemma boolean_inv_abst: ∀U,b0,b,M. {b}⇑ M = {b0}𝛌.U →
+                        ∃∃C. b = b0 & {b}⇑C = U & M = 𝛌.C.
+#U #b0 #b * normalize
+[ #i #H destruct
+| #A #H destruct /2 width=3/
+| #B #A #H destruct
+]
+qed-.
+
+lemma boolean_inv_appl: ∀W,U,b0,b,M. {b}⇑ M = {b0}@W.U →
+                        ∃∃D,C. b = b0 & {b}⇑D = W & {b}⇑C = U & M = @D.C.
+#W #U #b0 #b * normalize
+[ #i #H destruct
+| #A #H destruct
+| #B #A #H destruct /2 width=5/
+]
+qed-.
+
+(* Note: the carrier (underlying term) of a subset of subterms *)
+let rec carrier F on F ≝ match F with
+[ SVRef _ i   ⇒ #i
+| SAbst _ T   ⇒ 𝛌.(carrier T)
+| SAppl _ V T ⇒ @(carrier V).(carrier T)
+].
+
+interpretation "carrier (subterms)"
+   'ProjectDown F = (carrier F).
+
+notation "hvbox(⇓ term 46 F)"
+   non associative with precedence 46
+   for @{ 'ProjectDown $F }.
+
+lemma carrier_inv_vref: ∀j,F. ⇓F = #j → ∃b. F = {b}#j.
+#j * normalize
+[ #b #i #H destruct /2 width=2/
+| #b #T #H destruct
+| #b #V #T #H destruct
+]
+qed-.
+
+lemma carrier_inv_abst: ∀C,F. ⇓F = 𝛌.C → ∃∃b,U. ⇓U = C & F = {b}𝛌.U.
+#C * normalize
+[ #b #i #H destruct
+| #b #T #H destruct /2 width=4/
+| #b #V #T #H destruct
+]
+qed-.
+
+lemma carrier_inv_appl: ∀D,C,F. ⇓F = @D.C →
+                        ∃∃b,W,U. ⇓W = D & ⇓U = C & F = {b}@W.U.
+#D #C * normalize
+[ #b #i #H destruct
+| #b #T #H destruct
+| #b #V #T #H destruct /2 width=6/
+]
+qed-.
+
+definition mk_boolean: bool → subterms → subterms ≝
+   λb,F. {b}⇑⇓F.
+
+interpretation "make boolean (subterms)"
+   'ProjectSame b F = (mk_boolean b F).
+
+notation "hvbox( { term 46 b } ⇕ break term 46 F)"
+   non associative with precedence 46
+   for @{ 'ProjectSame $b $F }.
+
+lemma mk_boolean_inv_vref: ∀j,b0,b,F. {b}⇕ F = {b0}#j →
+                           ∃∃b1. b = b0 & F = {b1}#j.
+#j #b0 #b #F #H
+elim (boolean_inv_vref … H) -H #H0 #H
+elim (carrier_inv_vref … H) -H /2 width=2/
+qed-.
+
+lemma mk_boolean_inv_abst: ∀U,b0,b,F. {b}⇕ F = {b0}𝛌.U →
+                           ∃∃b1,T. b = b0 & {b}⇕T = U & F = {b1}𝛌.T.
+#U #b0 #b #F #H
+elim (boolean_inv_abst … H) -H #C #H0 #H1 #H
+elim (carrier_inv_abst … H) -H #b1 #U1 #H3 destruct /2 width=4/
+qed-.
+
+lemma mk_boolean_inv_appl: ∀W,U,b0,b,F. {b}⇕ F = {b0}@W.U →
+                           ∃∃b1,V,T. b = b0 & {b}⇕V = W & {b}⇕T = U & F = {b1}@V.T.
+#W #U #b0 #b #F #H
+elim (boolean_inv_appl … H) -H #D #C #H0 #H1 #H2 #H
+elim (carrier_inv_appl … H) -H #b1 #W1 #U1 #H3 #H4 destruct /2 width=6/
+qed-.
diff --git a/matita/matita/contribs/lambda/subterms/subterms.ma b/matita/matita/contribs/lambda/subterms/subterms.ma
index 565ed833a..909515122 100644
--- a/matita/matita/contribs/lambda/subterms/subterms.ma
+++ b/matita/matita/contribs/lambda/subterms/subterms.ma
@@ -13,7 +13,6 @@
 (**************************************************************************)
 
 include "background/preamble.ma".
-include "background/notation.ma".
 
 (* SUBSETS OF SUBTERMS ******************************************************)
 
diff --git a/matita/matita/contribs/lambda/terms/delifting_substitution.ma b/matita/matita/contribs/lambda/terms/delifting_substitution.ma
index 7926c3948..3603fc031 100644
--- a/matita/matita/contribs/lambda/terms/delifting_substitution.ma
+++ b/matita/matita/contribs/lambda/terms/delifting_substitution.ma
@@ -17,30 +17,30 @@ include "terms/lift.ma".
 (* DELIFTING SUBSTITUTION ***************************************************)
 
 (* Policy: depth (level) metavariables: d, e (as for lift) *)
-let rec dsubst D d M on M ≝ match M with
-[ VRef i   ⇒ tri … i d (#i) (↑[i] D) (#(i-1))
-| Abst A   ⇒ 𝛌. (dsubst D (d+1) A)
-| Appl B A ⇒ @ (dsubst D d B). (dsubst D d A)
+let rec dsubst N d M on M ≝ match M with
+[ VRef i   ⇒ tri … i d (#i) (↑[i] N) (#(i-1))
+| Abst A   ⇒ 𝛌. (dsubst N (d+1) A)
+| Appl B A ⇒ @ (dsubst N d B). (dsubst N d A)
 ].
 
 interpretation "delifting substitution"
-   'DSubst D d M = (dsubst D d M).
+   'DSubst N d M = (dsubst N d M).
 
-lemma dsubst_vref_lt: ∀i,d,D. i < d → [d ↙ D] #i = #i.
+lemma dsubst_vref_lt: ∀i,d,N. i < d → [d ↙ N] #i = #i.
 normalize /2 width=1/
 qed.
 
-lemma dsubst_vref_eq: ∀i,D. [i ↙ D] #i = ↑[i]D.
+lemma dsubst_vref_eq: ∀i,N. [i ↙ N] #i = ↑[i]N.
 normalize //
 qed.
 
-lemma dsubst_vref_gt: ∀i,d,D. d < i → [d ↙ D] #i = #(i-1).
+lemma dsubst_vref_gt: ∀i,d,N. d < i → [d ↙ N] #i = #(i-1).
 normalize /2 width=1/
 qed.
 
-theorem dsubst_lift_le: ∀h,D,M,d1,d2. d2 ≤ d1 →
-                        [d2 ↙ ↑[d1 - d2, h] D] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ D] M.
-#h #D #M elim M -M
+theorem dsubst_lift_le: ∀h,N,M,d1,d2. d2 ≤ d1 →
+                        [d2 ↙ ↑[d1 - d2, h] N] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ N] M.
+#h #N #M elim M -M
 [ #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2
   [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
     >(dsubst_vref_lt … Hid2) >(lift_vref_lt … Hid1) >lift_vref_lt /2 width=1/
@@ -58,9 +58,9 @@ theorem dsubst_lift_le: ∀h,D,M,d1,d2. d2 ≤ d1 →
 ]
 qed.
 
-theorem dsubst_lift_be: ∀h,D,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
-                        [d2 ↙ D] ↑[d1, h + 1] M = ↑[d1, h] M.
-#h #D #M elim M -M
+theorem dsubst_lift_be: ∀h,N,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
+                        [d2 ↙ N] ↑[d1, h + 1] M = ↑[d1, h] M.
+#h #N #M elim M -M
 [ #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
   [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
     >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/
@@ -75,9 +75,9 @@ theorem dsubst_lift_be: ∀h,D,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
 ]
 qed.
 
-theorem dsubst_lift_ge: ∀h,D,M,d1,d2. d1 + h ≤ d2 →
-                        [d2 ↙ D] ↑[d1, h] M = ↑[d1, h] [d2 - h ↙ D] M.
-#h #D #M elim M -M
+theorem dsubst_lift_ge: ∀h,N,M,d1,d2. d1 + h ≤ d2 →
+                        [d2 ↙ N] ↑[d1, h] M = ↑[d1, h] [d2 - h ↙ N] M.
+#h #N #M elim M -M
 [ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h
   [ >(dsubst_vref_lt … Hid2h) elim (lt_or_ge i d1) #Hid1
     [ lapply (lt_to_le_to_lt … (d1+h) Hid1 ?) -Hid2h // #Hid1h
@@ -102,9 +102,9 @@ theorem dsubst_lift_ge: ∀h,D,M,d1,d2. d1 + h ≤ d2 →
 ]
 qed.
 
-theorem dsubst_dsubst_ge: ∀D1,D2,M,d1,d2. d1 ≤ d2 →
-                          [d2 ↙ D2] [d1 ↙ D1] M = [d1 ↙ [d2 - d1 ↙ D2] D1] [d2 + 1 ↙ D2] M.
-#D1 #D2 #M elim M -M
+theorem dsubst_dsubst_ge: ∀N1,N2,M,d1,d2. d1 ≤ d2 →
+                          [d2 ↙ N2] [d1 ↙ N1] M = [d1 ↙ [d2 - d1 ↙ N2] N1] [d2 + 1 ↙ N2] M.
+#N1 #N2 #M elim M -M
 [ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1
   [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2
     >(dsubst_vref_lt … Hid1) >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/
@@ -125,30 +125,30 @@ theorem dsubst_dsubst_ge: ∀D1,D2,M,d1,d2. d1 ≤ d2 →
 ]
 qed.
 
-theorem dsubst_dsubst_lt: ∀D1,D2,M,d1,d2. d2 < d1 →
-                          [d2 ↙ [d1 - d2 -1 ↙ D1] D2] [d1 ↙ D1] M = [d1 - 1 ↙ D1] [d2 ↙ D2] M.
-#D1 #D2 #M #d1 #d2 #Hd21
+theorem dsubst_dsubst_lt: ∀N1,N2,M,d1,d2. d2 < d1 →
+                          [d2 ↙ [d1 - d2 -1 ↙ N1] N2] [d1 ↙ N1] M = [d1 - 1 ↙ N1] [d2 ↙ N2] M.
+#N1 #N2 #M #d1 #d2 #Hd21
 lapply (ltn_to_ltO … Hd21) #Hd1
 >dsubst_dsubst_ge in ⊢ (???%); /2 width=1/ <plus_minus_m_m //
 qed.
 
 definition dsubstable_dx: predicate (relation term) ≝ λR.
-                          ∀D,M1,M2. R M1 M2 → ∀d. R ([d ↙ D] M1) ([d ↙ D] M2).
+                          ∀N,M1,M2. R M1 M2 → ∀d. R ([d ↙ N] M1) ([d ↙ N] M2).
 
 definition dsubstable: predicate (relation term) ≝ λR.
-                       ∀D1,D2. R D1 D2 → ∀M1,M2. R M1 M2 → ∀d. R ([d ↙ D1] M1) ([d ↙ D2] M2).
+                       ∀N1,N2. R N1 N2 → ∀M1,M2. R M1 M2 → ∀d. R ([d ↙ N1] M1) ([d ↙ N2] M2).
 
 lemma star_dsubstable_dx: ∀R. dsubstable_dx R → dsubstable_dx (star … R).
-#R #HR #D #M1 #M2 #H elim H -M2 // /3 width=3/
+#R #HR #N #M1 #M2 #H elim H -M2 // /3 width=3/
 qed.
 
 lemma lstar_dsubstable_dx: ∀S,R. (∀a. dsubstable_dx (R a)) →
                            ∀l. dsubstable_dx (lstar S … R l).
-#S #R #HR #l #D #M1 #M2 #H
+#S #R #HR #l #N #M1 #M2 #H
 @(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
 qed.
 
 lemma star_dsubstable: ∀R. reflexive ? R →
                        dsubstable R → dsubstable (star … R).
-#R #H1R #H2 #D1 #D2 #H elim H -D2 /3 width=1/ /3 width=5/
+#R #H1R #H2 #N1 #N2 #H elim H -N2 /3 width=1/ /3 width=5/
 qed.
diff --git a/matita/matita/contribs/lambda/terms/sequential_reduction.ma b/matita/matita/contribs/lambda/terms/sequential_reduction.ma
index cfd1fbe7f..becaaac78 100644
--- a/matita/matita/contribs/lambda/terms/sequential_reduction.ma
+++ b/matita/matita/contribs/lambda/terms/sequential_reduction.ma
@@ -42,7 +42,7 @@ qed-.
 lemma sred_inv_abst: ∀M,N. M ↦ N → ∀C1. 𝛌.C1 = M →
                      ∃∃C2. C1 ↦ C2 & 𝛌.C2 = N.
 #M #N * -M -N
-[ #B #A #C #H destruct
+[ #B #A #C1 #H destruct
 | #A1 #A2 #HA12 #C1 #H destruct /2 width=3/
 | #B1 #B2 #A #_ #C1 #H destruct
 | #B #A1 #A2 #_ #C1 #H destruct
diff --git a/matita/matita/contribs/lambda/terms/term.ma b/matita/matita/contribs/lambda/terms/term.ma
index cf688d606..c831236a3 100644
--- a/matita/matita/contribs/lambda/terms/term.ma
+++ b/matita/matita/contribs/lambda/terms/term.ma
@@ -15,7 +15,6 @@
 (* Initial invocation: - Patience on us to gain peace and perfection! - *)
 
 include "background/preamble.ma".
-include "background/notation.ma".
 
 (* TERM STRUCTURE ***********************************************************)
 
diff --git a/matita/matita/contribs/lambda/xoa.conf.xml b/matita/matita/contribs/lambda/xoa.conf.xml
index 74b24697f..a0d089841 100644
--- a/matita/matita/contribs/lambda/xoa.conf.xml
+++ b/matita/matita/contribs/lambda/xoa.conf.xml
@@ -10,8 +10,12 @@
     <key name="include">basics/pts.ma</key>
     <key name="ex">2 2</key>
     <key name="ex">2 3</key>
+    <key name="ex">3 1</key>
     <key name="ex">3 2</key>
     <key name="ex">3 3</key>
+    <key name="ex">3 4</key>
+    <key name="ex">4 1</key>
+    <key name="ex">4 2</key>
     <key name="ex">4 3</key>
     <key name="or">3</key>
   </section>