From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Thu, 22 Sep 2011 12:25:07 +0000 (+0000)
Subject: - the confluence of context-senstitive parallel reduction (cpr) is closed!
X-Git-Tag: make_still_working~2269
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=95fe49b9bd546ee4f0d27dce7267d7285eb81b01;p=helm.git

- the confluence of context-senstitive parallel reduction (cpr) is closed!
- the theory of partial unfold on local environments (ltpss) is set up
---

diff --git a/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma b/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma
index 43b2174d9..ead47b546 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/grammar/item.ma
@@ -14,6 +14,7 @@
 
 (* THE FORMAL SYSTEM λδ - MATITA SOURCE FILES
  * Specification started: 2011 April 17
+ * Confluence of context-sensitive parallel reduction closed: 2011 September 21
  * Confluence of context-free parallel reduction closed: 2011 September 6
  * - Patience on me so that I gain peace and perfection! -
  * [ suggested invocation to start formal specifications with ]
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma
index f4b175925..0e123f64c 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma
@@ -13,13 +13,14 @@
 (**************************************************************************)
 
 include "Basic-2/grammar/cl_shift.ma".
+include "Basic-2/unfold/tpss.ma".
 include "Basic-2/reduction/tpr.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
 
 (* Basic-1: includes: pr2_delta1 *)
 definition cpr: lenv → relation term ≝
-   λL,T1,T2. ∃∃T. T1 ⇒ T & L ⊢ T [0, |L|] ≫ T2.
+   λL,T1,T2. ∃∃T. T1 ⇒ T & L ⊢ T [0, |L|] ≫* T2.
 
 interpretation
    "context-sensitive parallel reduction (term)"
@@ -31,26 +32,12 @@ interpretation
 lemma cpr_pr: ∀T1,T2. T1 ⇒ T2 → ∀L. L ⊢ T1 ⇒ T2.
 /2/ qed.
 
-lemma cpr_tps: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → L ⊢ T1 ⇒ T2.
+lemma cpr_tpss: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫* T2 → L ⊢ T1 ⇒ T2.
 /3 width=5/ qed.
 
 lemma cpr_refl: ∀L,T. L ⊢ T ⇒ T.
 /2/ qed.
 
-lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ⇒ V2 → T1 ⇒ T2 →
-                   L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
-#I #L #V1 #V2 #T1 #T2 * /3 width=5/
-qed.
-
-(* Basic-1: was only: pr2_gen_cbind *)
-lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ⇒ V2 → L. 𝕓{I} V2 ⊢ T1 ⇒ T2 →
-                   L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
-#I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2
-elim (tps_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
-lapply (tps_leq_repl_dx … HT0 (⋆. 𝕓{I} V2) ?) -HT0 /2/ #HT0
-/3 width=5/
-qed.
-
 (* Note: new property *)
 (* Basic-1: was only: pr2_thin_dx *) 
 lemma cpr_flat: ∀I,L,V1,V2,T1,T2.
@@ -58,11 +45,6 @@ lemma cpr_flat: ∀I,L,V1,V2,T1,T2.
 #I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 * /3 width=5/
 qed.
 
-lemma cpr_delta: ∀L,K,V,W,i.
-                 ↓[0, i] L ≡ K. 𝕓{Abbr} V → ↑[0, i + 1] V ≡ W → L ⊢ #i ⇒ W.
-/3/
-qed.
-
 lemma cpr_cast: ∀L,V,T1,T2.
                 L ⊢ T1 ⇒ T2 → L ⊢ 𝕔{Cast} V. T1 ⇒ T2.
 #L #V #T1 #T2 * /3/
@@ -73,25 +55,14 @@ qed.
 (* Basic-1: was: pr2_gen_csort *)
 lemma cpr_inv_atom: ∀T1,T2. ⋆ ⊢ T1 ⇒ T2 → T1 ⇒ T2.
 #T1 #T2 * #T #HT normalize #HT2
-<(tps_inv_refl_O2 … HT2) -HT2 //
+<(tpss_inv_refl_O2 … HT2) -HT2 //
 qed.
 
 (* Basic-1: was: pr2_gen_sort *)
 lemma cpr_inv_sort1: ∀L,T2,k. L ⊢ ⋆k ⇒ T2 → T2 = ⋆k.
 #L #T2 #k * #X #H
 >(tpr_inv_atom1 … H) -H #H
->(tps_inv_sort1 … H) -H //
-qed.
-
-(* Basic-1: was: pr2_gen_lref *)
-lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ⇒ T2 →
-                     T2 = #i ∨
-                     ∃∃K,T. ↓[0, i] L ≡ K. 𝕓{Abbr} T & ↑[0, i + 1] T ≡ T2 &
-                            i < |L|.
-#L #T2 #i * #X #H
->(tpr_inv_atom1 … H) -H #H
-elim (tps_inv_lref1 … H) -H /2/
-* #K #T #_ #Hi #HLK #HTT2 /3/
+>(tpss_inv_sort1 … H) -H //
 qed.
 (*
 (* Basic-1: was: pr2_gen_cast *)
@@ -104,26 +75,16 @@ elim (tpr_inv_cast1 … H) -H /3/
 * #V #T #HV1 #HT1 #H whd  (* >H in HU2; *) destruct -X;
 elim (tps_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H
 *)
-(* Basic forward lemmas *****************************************************)
-
-lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → L @ T1 ⇒ L @ T2.
-#L elim L -L
-[ /2/
-| normalize /3/
-].
-qed.
 
 (* Basic-1: removed theorems 5: 
             pr2_head_1 pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans
+   Basic-1: removed local theorems 3:
+            pr2_free_free pr2_free_delta pr2_delta_delta
 *)
 
 (*
 pr2/fwd pr2_gen_appl
 pr2/fwd pr2_gen_abbr
-pr2/pr2 pr2_confluence__pr2_free_free
-pr2/pr2 pr2_confluence__pr2_free_delta
-pr2/pr2 pr2_confluence__pr2_delta_delta
-pr2/pr2 pr2_confluence
 pr2/props pr2_change
 pr2/subst1 pr2_subst1
 pr2/subst1 pr2_gen_cabbr
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_cpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_cpr.ma
index d544918ac..086209007 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_cpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_cpr.ma
@@ -17,12 +17,42 @@ include "Basic-2/reduction/cpr.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
 
+(* Advanced properties ******************************************************)
+
+lemma cpr_bind_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ⇒ V2 → T1 ⇒ T2 →
+                   L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
+#I #L #V1 #V2 #T1 #T2 * #V #HV1 #HV2 #HT12 
+@ex2_1_intro [2: @(tpr_delta … HV1 HT12) | skip ] /2/ (* /3 width=5/ is too slow *)
+qed.
+
+(* Basic-1: was only: pr2_gen_cbind *)
+lemma cpr_bind_dx: ∀I,L,V1,V2,T1,T2. V1 ⇒ V2 → L. 𝕓{I} V2 ⊢ T1 ⇒ T2 →
+                   L ⊢ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
+#I #L #V1 #V2 #T1 #T2 #HV12 * #T #HT1 normalize #HT2
+elim (tpss_split_up … HT2 1 ? ?) -HT2 // #T0 <minus_n_O #HT0 normalize <minus_plus_m_m #HT02
+lapply (tpss_leq_repl_dx … HT0 (⋆. 𝕓{I} V2) ?) -HT0 /2/ #HT0
+lapply (tpss_tps … HT0) -HT0 #HT0
+@ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2/ ] (**) (* /3 width=5/ is too slow *)
+qed.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → L @ T1 ⇒ L @ T2.
+#L elim L -L
+[ /2/
+| normalize /3/
+].
+qed.
+
 (* Main properties **********************************************************)
-(*
+
 (* Basic-1: was: pr2_confluence *)
 theorem cpr_conf: ∀L,U0,T1,T2. L ⊢ U0 ⇒ T1 → L ⊢ U0 ⇒ T2 →
                   ∃∃T. L ⊢ T1 ⇒ T & L ⊢ T2 ⇒ T.
 #L #U0 #T1 #T2 * #U1 #HU01 #HUT1 * #U2 #HU02 #HUT2
 elim (tpr_conf … HU01 HU02) -U0 #U #HU1 #HU2 
+elim (tpr_tpss_ltpr ? L … HU1 … HUT1) -U1 // #U1 #HTU1 #HU1
+elim (tpr_tpss_ltpr ? L … HU2 … HUT2) -U2 // #U2 #HTU2 #HU2
+elim (tpss_conf_eq … HU1 … HU2) -U /3 width=5/
 qed.
-*)
+
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_lift.ma
index 89f84afaa..42703c24d 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_lift.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr_lift.ma
@@ -12,20 +12,44 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "Basic-2/unfold/tpss_lift.ma".
 include "Basic-2/reduction/tpr_lift.ma".
 include "Basic-2/reduction/cpr.ma".
 
 (* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
 
-(* Relocation properties ****************************************************)
-
-(* Basic-1: was: pr2_lift *)
+(* Advanced properties ******************************************************)
 
-(* Basic-1: was: pr2_gen_lift *)
+lemma cpr_delta: ∀L,K,V1,W1,W2,i.
+                 ↓[0, i] L ≡ K. 𝕓{Abbr} V1 → K ⊢ V1 [0, |L| - i - 1] ≫* W1 →
+                 ↑[0, i + 1] W1 ≡ W2 → L ⊢ #i ⇒ W2.
+#L #K #V1 #W1 #W2 #i #HLK #HVW1 #HW12
+@ex2_1_intro [2: // | skip | @tpss_subst /2 width=6/ ] (**) (* /4 width=6/ is too slow *)
+qed.
 
 (* Advanced inversion lemmas ************************************************)
 
+(* Basic-1: was: pr2_gen_lref *)
+lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ⇒ T2 →
+                     T2 = #i ∨
+                     ∃∃K,V1,T1. ↓[0, i] L ≡ K. 𝕓{Abbr} V1 &
+                                K ⊢ V1 [0, |L| - i - 1] ≫* T1 &
+                                ↑[0, i + 1] T1 ≡ T2 &
+                                i < |L|.
+#L #T2 #i * #X #H
+>(tpr_inv_atom1 … H) -H #H
+elim (tpss_inv_lref1 … H) -H /2/
+* /3 width=6/
+qed.
+
 (* Basic-1: was: pr2_gen_abst *)
 lemma cpr_inv_abst1: ∀V1,T1,U2. 𝕔{Abst} V1. T1 ⇒ U2 →
                      ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕔{Abst} V2. T2.
 /2/ qed.
+
+(* Relocation properties ****************************************************)
+
+(* Basic-1: was: pr2_lift *)
+
+(* Basic-1: was: pr2_gen_lift *)
+
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma
index 756527958..fce71d15a 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma
@@ -91,7 +91,7 @@ lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 →
                                  ⋆.  𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
                                  U2 = 𝕓{I} V2. T
                      ) ∨
-                     ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2 & I = Abbr.
+                     ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
 /2/ qed.
 
 (* Basic-1: was pr0_gen_abbr *)
@@ -100,7 +100,7 @@ lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕓{Abbr} V1. T1 ⇒ U2 →
                                  ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
                                  U2 = 𝕓{Abbr} V2. T
                       ) ∨
-                      ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2.
+                      ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2.
 #V1 #T1 #U2 #H
 elim (tpr_inv_bind1 … H) -H * /3 width=7/
 qed.
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma
index b7284718a..ac2112c7a 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tps.ma
@@ -12,20 +12,18 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "Basic-2/substitution/tps_tps.ma".
-include "Basic-2/substitution/ltps_tps.ma".
+include "Basic-2/unfold/ltpss_ltpss.ma".
 include "Basic-2/reduction/ltpr_drop.ma".
 
 (* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
 
-(* Note: the constant 1 comes from tps_subst *)
 (* Basic-1: was: pr0_subst1 *)
 lemma tpr_tps_ltpr: ∀T1,T2. T1 ⇒ T2 →
-                    ∀L1,d,U1. L1 ⊢ T1 [d, 1] ≫ U1 →
+                    ∀L1,d,e,U1. L1 ⊢ T1 [d, e] ≫ U1 →
                     ∀L2. L1 ⇒ L2 →
-                    ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, 1] ≫ U2.
+                    ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
 #T1 #T2 #H elim H -H T1 T2
-[ #I #L1 #d #X #H
+[ #I #L1 #d #e #X #H
   elim (tps_inv_atom1 … H) -H
   [ #H destruct -X /2/
   | * #K1 #V1 #i #Hdi #Hide #HLK1 #HVU1 #H #L2 #HL12 destruct -I;
@@ -33,42 +31,43 @@ lemma tpr_tps_ltpr: ∀T1,T2. T1 ⇒ T2 →
     elim (ltpr_inv_pair1 … H) -H #K2 #V2 #_ #HV12 #H destruct -X;
     elim (lift_total V2 0 (i+1)) #U2 #HVU2
     lapply (tpr_lift … HV12 … HVU1 … HVU2) -HV12 HVU1 #HU12
-    @ex2_1_intro [2: @HU12 | skip | /2/ ] (**) (* /3 width=6/ is too slow *)
+    @ex2_1_intro [2: @HU12 | skip | /3/ ] (**) (* /4 width=6/ is too slow *)
   ]
-| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #X #H #L2 #HL12
+| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct -X;
   elim (IHV12 … HVW1 … HL12) -IHV12 HVW1;
   elim (IHT12 … HTU1 … HL12) -IHT12 HTU1 HL12 /3 width=5/
-| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #X #H #L2 #HL12
+| #V1 #V2 #W #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X;
   elim (tps_inv_bind1 … HY) -HY #WW #TT1 #_ #HTT1 #H destruct -Y;
   elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
   elim (IHT12 … HTT1 (L2. 𝕓{Abst} WW) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
-  lapply (tps_leq_repl_dx … HTT2 (L2. 𝕓{Abbr} VV2) ?) -HTT2 /3 width=5/
-| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #X #H #L2 #HL12
+  lapply (tpss_leq_repl_dx … HTT2 (L2. 𝕓{Abbr} VV2) ?) -HTT2 /3 width=5/
+| #I #V1 #V2 #T1 #T2 #U2 #HV12 #_ #HTU2 #IHV12 #IHT12 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_bind1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X;
   elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
   elim (IHT12 … HTT1 (L2. 𝕓{I} VV2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
-  elim (tps_conf_neq … HTT2 … HTU2 ?) -HTT2 HTU2 T2 /2/ #T2 #HTT2 #HUT2
+  elim (tpss_strip_neq … HTT2 … HTU2 ?) -HTT2 HTU2 T2 /2/ #T2 #HTT2 #HUT2
   lapply (tps_leq_repl_dx … HTT2 (L2. 𝕓{I} V2) ?) -HTT2 /2/ #HTT2
-  elim (ltps_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) 1 ?) -HTT2 /2/ #W2 #HTTW2 #HTW2
-  lapply (tps_leq_repl_dx … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2/ #HTTW2
-  lapply (tps_trans_ge … HUT2 … HTW2 ?) -HUT2 HTW2 // #HUW2
-  /3 width=5/
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #X #H #L2 #HL12
+  elim (ltpss_tps_conf … HTT2 (L2. 𝕓{I} VV2) (d + 1) e ?) -HTT2 /2/ #W2 #HTTW2 #HTW2 
+  lapply (tpss_leq_repl_dx … HTTW2 (⋆. 𝕓{I} VV2) ?) -HTTW2 /2/ #HTTW2
+  lapply (tpss_tps … HTTW2) -HTTW2 #HTTW2
+  lapply (tpss_leq_repl_dx … HTW2 (L2. 𝕓{I} VV2) ?) -HTW2 /2/ #HTW2
+  lapply (tpss_trans_eq … HUT2 … HTW2) -HUT2 HTW2 /3 width=5/
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_flat1 … H) -H #VV1 #Y #HVV1 #HY #HX destruct -X;
   elim (tps_inv_bind1 … HY) -HY #WW1 #TT1 #HWW1 #HTT1 #H destruct -Y;
   elim (IHV12 … HVV1 … HL12) -IHV12 HVV1 #VV2 #HVV12 #HVV2
   elim (IHW12 … HWW1 … HL12) -IHW12 HWW1 #WW2 #HWW12 #HWW2
   elim (IHT12 … HTT1 (L2. 𝕓{Abbr} WW2) ?) -IHT12 HTT1 /2/ -HL12 #TT2 #HTT12 #HTT2
   elim (lift_total VV2 0 1) #VV #H2VV
-  lapply (tps_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 H2VV ?) -HVV2 HV2 /2/ #HVV
-  @ex2_1_intro [2: @tpr_theta |1: skip |3: @tps_bind [2: @tps_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
-| #V1 #TT1 #T1 #T2 #HT1 #_ #IHT12 #L1 #d #X #H #L2 #HL12
+  lapply (tpss_lift_ge … HVV2 (L2. 𝕓{Abbr} WW2) … HV2 … H2VV) -HVV2 HV2 /2/ #HVV
+  @ex2_1_intro [2: @tpr_theta |1: skip |3: @tpss_bind [2: @tpss_flat ] ] /width=11/ (**) (* /4 width=11/ is too slow *)
+| #V1 #TT1 #T1 #T2 #HT1 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_bind1 … H) -H #V2 #TT2 #HV12 #HTT12 #H destruct -X;
   elim (tps_inv_lift1_ge … HTT12 L1 … HT1 ?) -HTT12 HT1 /2/ #T2 #HT12 #HTT2
   elim (IHT12 … HT12 … HL12) -IHT12 HT12 HL12 <minus_plus_m_m /3/
-| #V1 #T1 #T2 #_ #IHT12 #L1 #d #X #H #L2 #HL12
+| #V1 #T1 #T2 #_ #IHT12 #L1 #d #e #X #H #L2 #HL12
   elim (tps_inv_flat1 … H) -H #VV1 #TT1 #HVV1 #HTT1 #H destruct -X;
   elim (IHT12 … HTT1 … HL12) -IHT12 HTT1 HL12 /3/
 ]
@@ -77,4 +76,17 @@ qed.
 lemma tpr_tps_bind: ∀I,V1,V2,T1,T2,U1. V1 ⇒ V2 → T1 ⇒ T2 →
                     ⋆. 𝕓{I} V1 ⊢ T1 [0, 1] ≫ U1 →
                     ∃∃U2. U1 ⇒ U2 & ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ U2.
-/3 width=7/ qed.
+#I #V1 #V2 #T1 #T2 #U1 #HV12 #HT12 #HTU1
+elim (tpr_tps_ltpr … HT12 … HTU1 (⋆. 𝕓{I} V2) ?) -HT12 HTU1 /3/
+qed.
+
+lemma tpr_tpss_ltpr: ∀L1,L2. L1 ⇒ L2 → ∀T1,T2. T1 ⇒ T2 →
+                     ∀d,e,U1. L1 ⊢ T1 [d, e] ≫* U1 →
+                     ∃∃U2. U1 ⇒ U2 & L2 ⊢ T2 [d, e] ≫* U2.
+#L1 #L2 #HL12 #T1 #T2 #HT12 #d #e #U1 #HTU1 @(tpss_ind … HTU1) -U1
+[ /2/
+| -HT12 #U #U1 #_ #HU1 * #T #HUT #HT2
+  elim (tpr_tps_ltpr … HUT … HU1 … HL12) -HUT HU1 HL12 #U2 #HU12 #HTU2
+  lapply (tpss_trans_eq … HT2 … HTU2) -T /2/
+]
+qed.  
\ No newline at end of file
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss.ma b/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss.ma
new file mode 100644
index 000000000..4f2062a14
--- /dev/null
+++ b/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss.ma
@@ -0,0 +1,107 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "Basic-2/substitution/ltps.ma".
+include "Basic-2/unfold/tpss.ma".
+
+(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
+
+definition ltpss: nat → nat → relation lenv ≝
+                  λd,e. TC … (ltps d e).
+
+interpretation "partial unfold (local environment)"
+   'PSubstStar L1 d e L2 = (ltpss d e L1 L2).
+
+(* Basic eliminators ********************************************************)
+
+lemma ltpss_ind: ∀d,e,L1. ∀R: lenv → Prop. R L1 →
+                 (∀L,L2. L1 [d, e] ≫* L → L [d, e] ≫ L2 → R L → R L2) →
+                 ∀L2. L1 [d, e] ≫* L2 → R L2.
+#d #e #L1 #R #HL1 #IHL1 #L2 #HL12 @(TC_star_ind … HL1 IHL1 … HL12) //
+qed.
+
+(* Basic properties *********************************************************)
+
+lemma ltpss_strap: ∀L1,L,L2,d,e.
+                   L1 [d, e] ≫ L → L [d, e] ≫* L2 → L1 [d, e] ≫* L2. 
+/2/ qed.
+
+lemma ltpss_refl: ∀L,d,e. L [d, e] ≫* L.
+/2/ qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma ltpss_inv_refl_O2: ∀d,L1,L2. L1 [d, 0] ≫* L2 → L1 = L2.
+#d #L1 #L2 #H @(ltpss_ind … H) -L2 //
+#L #L2 #_ #HL2 #IHL <(ltps_inv_refl_O2 … HL2) -HL2 //
+qed.
+
+lemma ltpss_inv_atom1: ∀d,e,L2. ⋆ [d, e] ≫* L2 → L2 = ⋆.
+#d #e #L2 #H @(ltpss_ind … H) -L2 //
+#L #L2 #_ #HL2 #IHL destruct -L
+>(ltps_inv_atom1 … HL2) -HL2 //
+qed.
+(*
+fact ltps_inv_atom2_aux: ∀d,e,L1,L2.
+                         L1 [d, e] ≫ L2 → L2 = ⋆ → L1 = ⋆.
+#d #e #L1 #L2 * -d e L1 L2
+[ //
+| #L #I #V #H destruct
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H destruct
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H destruct
+]
+qed.
+
+lemma drop_inv_atom2: ∀d,e,L1. L1 [d, e] ≫ ⋆ → L1 = ⋆.
+/2 width=5/ qed.
+
+fact ltps_inv_tps22_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → d = 0 → 0 < e →
+                         ∀K2,I,V2. L2 = K2. 𝕓{I} V2 →
+                         ∃∃K1,V1. K1 [0, e - 1] ≫ K2 &
+                                  K2 ⊢ V1 [0, e - 1] ≫ V2 &
+                                  L1 = K1. 𝕓{I} V1.
+#d #e #L1 #L2 * -d e L1 L2
+[ #d #e #_ #_ #K1 #I #V1 #H destruct
+| #L1 #I #V #_ #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #_ #_ #K2 #J #W2 #H destruct -L2 I V2 /2 width=5/
+| #L1 #L2 #I #V1 #V2 #d #e #_ #_ #H elim (plus_S_eq_O_false … H)
+]
+qed.
+
+lemma ltps_inv_tps22: ∀e,L1,K2,I,V2. L1 [0, e] ≫ K2. 𝕓{I} V2 → 0 < e →
+                      ∃∃K1,V1. K1 [0, e - 1] ≫ K2 & K2 ⊢ V1 [0, e - 1] ≫ V2 &
+                               L1 = K1. 𝕓{I} V1.
+/2 width=5/ qed.
+
+fact ltps_inv_tps12_aux: ∀d,e,L1,L2. L1 [d, e] ≫ L2 → 0 < d →
+                         ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
+                         ∃∃K1,V1. K1 [d - 1, e] ≫ K2 &
+                                  K2 ⊢ V1 [d - 1, e] ≫ V2 &
+                                  L1 = K1. 𝕓{I} V1.
+#d #e #L1 #L2 * -d e L1 L2
+[ #d #e #_ #I #K2 #V2 #H destruct
+| #L #I #V #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #e #_ #_ #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #_ #J #K2 #W2 #H destruct -L2 I V2
+  /2 width=5/
+]
+qed.
+
+lemma ltps_inv_tps12: ∀L1,K2,I,V2,d,e. L1 [d, e] ≫ K2. 𝕓{I} V2 → 0 < d →
+                      ∃∃K1,V1. K1 [d - 1, e] ≫ K2 &
+                                  K2 ⊢ V1 [d - 1, e] ≫ V2 &
+                                  L1 = K1. 𝕓{I} V1.
+/2/ qed.
+
+*)
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss_ltpss.ma b/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss_ltpss.ma
new file mode 100644
index 000000000..0bf94ae76
--- /dev/null
+++ b/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss_ltpss.ma
@@ -0,0 +1,55 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "Basic-2/unfold/ltpss_tpss.ma".
+
+(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
+
+(* Main properties **********************************************************)
+
+theorem ltpss_trans_eq: ∀L1,L,L2,d,e.
+                        L1 [d, e] ≫* L → L [d, e] ≫* L2 → L1 [d, e] ≫* L2. 
+/2/ qed.
+
+lemma ltpss_tpss2: ∀L1,L2,I,V1,V2,e.
+                   L1 [0, e] ≫* L2 → L2 ⊢ V1 [0, e] ≫* V2 →
+                   L1. 𝕓{I} V1 [0, e + 1] ≫* L2. 𝕓{I} V2.
+#L1 #L2 #I #V1 #V2 #e #HL12 #H @(tpss_ind … H) -V2
+[ /2/
+| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2/
+]
+qed.
+
+lemma ltpss_tpss2_lt: ∀L1,L2,I,V1,V2,e.
+                      L1 [0, e - 1] ≫* L2 → L2 ⊢ V1 [0, e - 1] ≫* V2 →
+                      0 < e → L1. 𝕓{I} V1 [0, e] ≫* L2. 𝕓{I} V2.
+#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
+>(plus_minus_m_m e 1) /2/
+qed.
+
+lemma ltpss_tpss1: ∀L1,L2,I,V1,V2,d,e.
+                   L1 [d, e] ≫* L2 → L2 ⊢ V1 [d, e] ≫* V2 →
+                   L1. 𝕓{I} V1 [d + 1, e] ≫* L2. 𝕓{I} V2.
+#L1 #L2 #I #V1 #V2 #d #e #HL12 #H @(tpss_ind … H) -V2
+[ /2/
+| #V #V2 #_ #HV2 #IHV @(ltpss_trans_eq … IHV) /2/
+]
+qed.
+
+lemma ltpss_tpss1_lt: ∀L1,L2,I,V1,V2,d,e.
+                      L1 [d - 1, e] ≫* L2 → L2 ⊢ V1 [d - 1, e] ≫* V2 →
+                      0 < d → L1. 𝕓{I} V1 [d, e] ≫* L2. 𝕓{I} V2.
+#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
+>(plus_minus_m_m d 1) /2/
+qed.
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss_tpss.ma b/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss_tpss.ma
new file mode 100644
index 000000000..b8e425e63
--- /dev/null
+++ b/matita/matita/contribs/lambda-delta/Basic-2/unfold/ltpss_tpss.ma
@@ -0,0 +1,169 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "Basic-2/unfold/tpss_ltps.ma".
+include "Basic-2/unfold/ltpss.ma".
+
+(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
+
+(* Properties concerning partial unfold on terms ****************************)
+
+lemma ltpss_tpss_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
+                           ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫* U2 →
+                           d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ≫* U2.
+#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 //
+#L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
+lapply (ltps_tpss_trans_ge … HL0 HTU2) -HL0 HTU2 /2/
+qed.
+
+lemma ltpss_tps_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
+                          ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ≫ U2 →
+                          d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ≫* U2.
+#L1 #L0 #d1 #e1 #HL10 #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
+@(ltpss_tpss_trans_ge … HL10 … Hde1d2) /2/ (**) (* /3 width=6/ is too slow *)
+qed.
+
+lemma ltpss_tpss_trans_eq: ∀L0,L1,d,e. L0 [d, e] ≫* L1 →
+                           ∀T2,U2. L1 ⊢ T2 [d, e] ≫* U2 → L0 ⊢ T2 [d, e] ≫* U2.
+#L0 #L1 #d #e #H @(ltpss_ind … H) -L1
+[ /2/
+| #L #L1 #_ #HL1 #IHL #T2 #U2 #HTU2
+  lapply (ltps_tpss_trans_eq … HL1 HTU2) -HL1 HTU2 /2/
+]
+qed.
+
+lemma ltpss_tps_trans_eq: ∀L0,L1,d,e. L0 [d, e] ≫* L1 →
+                          ∀T2,U2. L1 ⊢ T2 [d, e] ≫ U2 → L0 ⊢ T2 [d, e] ≫* U2.
+/3/ qed.
+
+lemma ltpss_tpss_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 → 
+                          L0 ⊢ T2 [d2, e2] ≫* U2 → L0 [d1, e1] ≫* L1 →
+                          L1 ⊢ T2 [d2, e2] ≫* U2.
+#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpss_ind … H) -L1
+[ //
+| -HTU2 #L #L1 #_ #HL1 #IHL
+  lapply (ltps_tpss_conf_ge … HL1 IHL) -HL1 IHL //
+]
+qed.
+
+lemma ltpss_tps_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 → 
+                         L0 ⊢ T2 [d2, e2] ≫ U2 → L0 [d1, e1] ≫* L1 →
+                         L1 ⊢ T2 [d2, e2] ≫* U2.
+#L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #HL01
+@(ltpss_tpss_conf_ge … Hde1d2 … HL01) /2/ (**) (* /3 width=6/ is too slow *)
+qed.
+
+lemma ltpss_tpss_conf_eq: ∀L0,L1,T2,U2,d,e.
+                          L0 ⊢ T2 [d, e] ≫* U2 → L0 [d, e] ≫* L1 →
+                          ∃∃T. L1 ⊢ T2 [d, e] ≫* T & L1 ⊢ U2 [d, e] ≫* T.
+#L0 #L1 #T2 #U2 #d #e #HTU2 #H @(ltpss_ind … H) -L1
+[ /2/
+| -HTU2 #L #L1 #_ #HL1 * #W2 #HTW2 #HUW2
+  elim (ltps_tpss_conf … HL1 HTW2) -HTW2 #T #HT2 #HW2T
+  elim (ltps_tpss_conf … HL1 HUW2) -HL1 HUW2 #U #HU2 #HW2U
+  elim (tpss_conf_eq … HW2T … HW2U) -HW2T HW2U #V #HTV #HUV
+  lapply (tpss_trans_eq … HT2 … HTV) -T;
+  lapply (tpss_trans_eq … HU2 … HUV) -U /2/
+]
+qed.
+
+lemma ltpss_tps_conf_eq: ∀L0,L1,T2,U2,d,e.
+                         L0 ⊢ T2 [d, e] ≫ U2 → L0 [d, e] ≫* L1 →
+                         ∃∃T. L1 ⊢ T2 [d, e] ≫* T & L1 ⊢ U2 [d, e] ≫* T.
+/3/ qed.
+
+lemma ltpss_tpss_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫* T2 →
+                       ∀L2,ds,es. L1 [ds, es] ≫* L2 → 
+                       ∃∃T. L2 ⊢ T1 [d, e] ≫* T & L1 ⊢ T2 [ds, es] ≫* T.
+#L1 #T1 #T2 #d #e #HT12 #L2 #ds #es #H @(ltpss_ind … H) -L2
+[ /3/
+| #L #L2 #HL1 #HL2 * #T #HT1 #HT2
+  elim (ltps_tpss_conf … HL2 HT1) -HT1 #T0 #HT10 #HT0
+  lapply (ltps_tpss_trans_eq … HL2 … HT0) -HL2 HT0 #HT0
+  lapply (ltpss_tpss_trans_eq … HL1 … HT0) -HL1 HT0 #HT0
+  lapply (tpss_trans_eq … HT2 … HT0) -T /2/
+]
+qed.
+
+lemma ltpss_tps_conf: ∀L1,T1,T2,d,e. L1 ⊢ T1 [d, e] ≫ T2 →
+                      ∀L2,ds,es. L1 [ds, es] ≫* L2 → 
+                      ∃∃T. L2 ⊢ T1 [d, e] ≫* T & L1 ⊢ T2 [ds, es] ≫* T.
+/3/ qed.
+
+(* Advanced properties ******************************************************)
+
+lemma ltpss_tps2: ∀L1,L2,I,e.
+                  L1 [0, e] ≫* L2 → ∀V1,V2. L2 ⊢ V1 [0, e] ≫ V2 →
+                  L1. 𝕓{I} V1 [0, e + 1] ≫* L2. 𝕓{I} V2.
+#L1 #L2 #I #e #H @(ltpss_ind … H) -L2
+[ /3/
+| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
+  elim (ltps_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2
+  lapply (IHL … HV1) -IHL HV1 #HL1
+  @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+]
+qed.
+
+lemma ltpss_tps2_lt: ∀L1,L2,I,V1,V2,e.
+                     L1 [0, e - 1] ≫* L2 → L2 ⊢ V1 [0, e - 1] ≫ V2 →
+                     0 < e → L1. 𝕓{I} V1 [0, e] ≫* L2. 𝕓{I} V2.
+#L1 #L2 #I #V1 #V2 #e #HL12 #HV12 #He
+>(plus_minus_m_m e 1) /2/
+qed.
+
+lemma ltpss_tps1: ∀L1,L2,I,d,e. L1 [d, e] ≫* L2 →
+                  ∀V1,V2. L2 ⊢ V1 [d, e] ≫ V2 →
+                  L1. 𝕓{I} V1 [d + 1, e] ≫* L2. 𝕓{I} V2.
+#L1 #L2 #I #d #e #H @(ltpss_ind … H) -L2
+[ /3/
+| #L #L2 #_ #HL2 #IHL #V1 #V2 #HV12
+  elim (ltps_tps_trans … HV12 … HL2) -HV12 #V #HV1 #HV2
+  lapply (IHL … HV1) -IHL HV1 #HL1
+  @step /2 width=5/ (**) (* /3 width=5/ is too slow *)
+]
+qed.
+
+lemma ltpss_tps1_lt: ∀L1,L2,I,V1,V2,d,e.
+                     L1 [d - 1, e] ≫* L2 → L2 ⊢ V1 [d - 1, e] ≫ V2 →
+                     0 < d → L1. 𝕓{I} V1 [d, e] ≫* L2. 𝕓{I} V2.
+#L1 #L2 #I #V1 #V2 #d #e #HL12 #HV12 #Hd
+>(plus_minus_m_m d 1) /2/
+qed.
+
+(* Advanced forward lemmas **************************************************)
+
+lemma ltpss_fwd_tpsa21: ∀e,K1,I,V1,L2. 0 < e → K1. 𝕓{I} V1 [0, e] ≫* L2 →
+                        ∃∃K2,V2. K1 [0, e - 1] ≫* K2 & K1 ⊢ V1 [0, e - 1] ≫* V2 &
+                                 L2 = K2. 𝕓{I} V2.
+#e #K1 #I #V1 #L2 #He #H @(ltpss_ind … H) -L2
+[ /2 width=5/
+| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct -L;
+  elim (ltps_inv_tps21 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H
+  lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2
+  lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/
+]
+qed.
+
+lemma ltpss_fwd_tpss11: ∀d,e,I,K1,V1,L2. 0 < d → K1. 𝕓{I} V1 [d, e] ≫* L2 →
+                        ∃∃K2,V2. K1 [d - 1, e] ≫* K2 &
+                                 K1 ⊢ V1 [d - 1, e] ≫* V2 &
+                                 L2 = K2. 𝕓{I} V2.
+#d #e #K1 #I #V1 #L2 #Hd #H @(ltpss_ind … H) -L2
+[ /2 width=5/
+| #L #L2 #_ #HL2 * #K #V #HK1 #HV1 #H destruct -L;
+  elim (ltps_inv_tps11 … HL2 ?) -HL2 // #K2 #V2 #HK2 #HV2 #H
+  lapply (ltps_tps_trans_eq … HV2 … HK2) -HV2 #HV2
+  lapply (ltpss_tpss_trans_eq … HK1 … HV2) -HV2 #HV2 /3 width=5/
+]
+qed.
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_tpss.ma b/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_tpss.ma
index 5cc6b38b7..a84928453 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_tpss.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/unfold/tpss_tpss.ma
@@ -19,6 +19,12 @@ include "Basic-2/unfold/tpss_lift.ma".
 
 (* Advanced properties ******************************************************)
 
+lemma tpss_tps: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫* T2 → L ⊢ T1 [d, 1] ≫ T2.
+#L #T1 #T2 #d #H @(tpss_ind … H) -H T2 //
+#T #T2 #_ #HT2 #IHT1
+lapply (tps_trans_ge … IHT1 … HT2 ?) //
+qed.
+
 lemma tpss_strip_eq: ∀L,T0,T1,d1,e1. L ⊢ T0 [d1, e1] ≫* T1 →
                      ∀T2,d2,e2. L ⊢ T0 [d2, e2] ≫ T2 →
                      ∃∃T. L ⊢ T1 [d2, e2] ≫ T & L ⊢ T2 [d1, e1] ≫* T.