From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 24 Aug 2011 17:48:10 +0000 (+0000)
Subject: one reduction rule (tpr) was redundant
X-Git-Tag: make_still_working~2326
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7c7d06e172313059f73302fab2aab59efbf1f419;p=helm.git

one reduction rule (tpr) was redundant
---

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 f41999e45..090c6cf6f 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/cpr.ma
@@ -33,7 +33,18 @@ lemma cpr_tps: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → L ⊢ T1 ⇒ T2.
 
 lemma cpr_refl: ∀L,T. L ⊢ T ⇒ T.
 /2/ qed.
-
+(*
+(* NOTE: new property *)
+lemma cpr_bind: ∀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
+@ex2_1_intro
+[3: @tps_bind [3: // |4: @HT02 |1,2: skip ]
+|1: skip
+|2: @tpr_delta [2: @HV12 |3: @HT1 |1: skip |6: ]
+]   
+*)
 (* NOTE: new property *)
 lemma cpr_flat: ∀I,L,V1,V2,T1,T2.
                 L ⊢ V1 ⇒ V2 → L ⊢ T1 ⇒ T2 → L ⊢ 𝕗{I} V1. T1 ⇒ 𝕗{I} V2. T2.
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 42d4b4e94..8e162bb2c 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr.ma
@@ -19,16 +19,14 @@ include "Basic-2/substitution/tps.ma".
 inductive tpr: term → term → Prop ≝
 | tpr_sort : ∀k. tpr (⋆k) (⋆k)
 | tpr_lref : ∀i. tpr (#i) (#i)
-| tpr_bind : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
-             tpr (𝕓{I} V1. T1) (𝕓{I} V2. T2)
 | tpr_flat : ∀I,V1,V2,T1,T2. tpr V1 V2 → tpr T1 T2 →
              tpr (𝕗{I} V1. T1) (𝕗{I} V2. T2)
 | tpr_beta : ∀V1,V2,W,T1,T2.
              tpr V1 V2 → tpr T1 T2 →
              tpr (𝕚{Appl} V1. 𝕚{Abst} W. T1) (𝕚{Abbr} V2. T2)
-| tpr_delta: ∀V1,V2,T1,T2,T.
-             tpr V1 V2 → tpr T1 T2 → ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T →
-             tpr (𝕚{Abbr} V1. T1) (𝕚{Abbr} V2. T)
+| tpr_delta: ∀I,V1,V2,T1,T2,T.
+             tpr V1 V2 → tpr T1 T2 → ⋆.  𝕓{I} V2 ⊢ T2 [0, 1] ≫ T →
+             tpr (𝕚{I} V1. T1) (𝕚{I} V2. T)
 | tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
              tpr V1 V2 → ↑[0,1] V2 ≡ V → tpr W1 W2 → tpr T1 T2 →
              tpr (𝕚{Appl} V1. 𝕚{Abbr} W1. T1) (𝕚{Abbr} W2. 𝕚{Appl} V. T2)
@@ -43,6 +41,10 @@ interpretation
 
 (* Basic properties *********************************************************)
 
+lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ⇒ V2 → T1 ⇒ T2 →
+                                𝕓{I} V1. T1 ⇒  𝕓{I} V2. T2.
+/2/ qed.
+
 lemma tpr_refl: ∀T. T ⇒ T.
 #T elim T -T //
 #I elim I -I /2/
@@ -55,9 +57,8 @@ lemma tpr_inv_sort1_aux: ∀U1,U2. U1 ⇒ U2 → ∀k. U1 = ⋆k → U2 = ⋆k.
 [ #k0 #k #H destruct -k0 //
 | #i #k #H destruct
 | #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
-| #I #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
 | #V1 #V2 #W #T1 #T2 #_ #_ #k #H destruct
-| #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct
+| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #k #H destruct
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #k #H destruct
 | #V #T #T1 #T2 #_ #_ #k #H destruct
 | #V #T1 #T2 #_ #k #H destruct
@@ -72,9 +73,8 @@ lemma tpr_inv_lref1_aux: ∀U1,U2. U1 ⇒ U2 → ∀i. U1 = #i → U2 = #i.
 [ #k #i #H destruct
 | #j #i #H destruct -j //
 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
-| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
 | #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
-| #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
 | #V #T #T1 #T2 #_ #_ #i #H destruct
 | #V #T1 #T2 #_ #i #H destruct
@@ -84,62 +84,40 @@ qed.
 lemma tpr_inv_lref1: ∀i,U2. #i ⇒ U2 → U2 = #i.
 /2/ qed.
 
-lemma tpr_inv_abbr1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abbr} V1. T1 →
-                         ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abbr} V2. T2
-                          | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
-                                       ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
-                                       U2 = 𝕚{Abbr} V2. T
-                          | ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2.
-#U1 #U2 * -U1 U2
-[ #k #V #T #H destruct
-| #i #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
-| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
-| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
-| #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -V1 T1 /3 width=7/
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
-| #V #T #T1 #T2 #HT1 #HT12 #V0 #T0 #H destruct -V T /3/
-| #V #T1 #T2 #_ #V0 #T0 #H destruct
-]
-qed.
-
-lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕚{Abbr} V1. T1 ⇒ U2 →
-                     ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abbr} V2. T2
-                      | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
-                                   ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
-                                   U2 = 𝕚{Abbr} V2. T
-                      | ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2.
-/2/ qed.
-
-lemma tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abst} V1. T1 →
-                         ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2.
+lemma tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
+                         (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
+                                     ⋆.  𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
+                                     U2 = 𝕚{I} V2. T
+                          )∨
+                          ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
 #U1 #U2 * -U1 U2
-[ #k #V #T #H destruct
-| #i #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /2 width=5/
-| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
-| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
-| #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
-| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
-| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
-| #V #T1 #T2 #_ #V0 #T0 #H destruct
+[ #k #I #V #T #H destruct
+| #i #I #V #T #H destruct
+| #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
+| #V1 #V2 #W #T1 #T2 #_ #_ #I #V #T #H destruct
+| #I1 #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #I0 #V0 #T0 #H destruct -I1 V1 T1 /3 width=7/
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #I0 #V0 #T0 #H destruct
+| #V #T #T1 #T2 #HT1 #HT12 #I0 #V0 #T0 #H destruct -V T /3/
+| #V #T1 #T2 #_ #I0 #V0 #T0 #H destruct
 ]
 qed.
 
-lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕚{Abst} V1. T1 ⇒ U2 →
-                     ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2.
+lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 →
+                     (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
+                                 ⋆.  𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
+                                 U2 = 𝕚{I} V2. T
+                     ) ∨
+                     ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2 & I = Abbr.
 /2/ qed.
 
-lemma tpr_inv_bind1: ∀V1,T1,U2,I. 𝕓{I} V1. T1 ⇒ U2 →
-                     ∨∨ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕓{I} V2. T2
-                      | ∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
-                                   ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
-                                   U2 = 𝕚{Abbr} V2. T & I = Abbr
-                      | ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2 & I = Abbr.
-#V1 #T1 #U2 * #H
-[ elim (tpr_inv_abbr1 … H) -H * /3 width=7/
-| /3/
-]
+lemma tpr_inv_abbr1: ∀V1,T1,U2. 𝕚{Abbr} V1. T1 ⇒ U2 →
+                     (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
+                                 ⋆.  𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
+                                 U2 = 𝕚{Abbr} V2. T
+                      ) ∨
+                      ∃∃T. ↑[0,1] T ≡ T1 & tpr T U2.
+#V1 #T1 #U2 #H
+elim (tpr_inv_bind1 … H) -H * /3 width=7/
 qed.
 
 lemma tpr_inv_appl1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,U0. U1 = 𝕚{Appl} V1. U0 →
@@ -155,10 +133,9 @@ lemma tpr_inv_appl1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,U0. U1 = 𝕚{Appl} V1. U
 #U1 #U2 * -U1 U2
 [ #k #V #T #H destruct
 | #i #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
 | #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
 | #V1 #V2 #W #T1 #T2 #HV12 #HT12 #V #T #H destruct -V1 T /3 width=8/
-| #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
+| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #V0 #T0 #H
   destruct -V1 T0 /3 width=12/
 | #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
@@ -184,10 +161,9 @@ lemma tpr_inv_cast1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Cast} V1. T
 #U1 #U2 * -U1 U2
 [ #k #V #T #H destruct
 | #i #V #T #H destruct
-| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
 | #I #V1 #V2 #T1 #T2 #HV12 #HT12 #V #T #H destruct -I V1 T1 /3 width=5/
 | #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
-| #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
+| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #V0 #T0 #H destruct
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
 | #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
 | #V #T1 #T2 #HT12 #V0 #T0 #H destruct -V T1 /2/
@@ -226,9 +202,8 @@ lemma tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
 [ #k #i #H destruct
 | #j #i /2/
 | #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
-| #I #V1 #V2 #T1 #T2 #_ #_ #i #H destruct
 | #V1 #V2 #W #T1 #T2 #_ #_ #i #H destruct
-| #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
+| #I #V1 #V2 #T1 #T2 #T #_ #_ #_ #i #H destruct
 | #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #i #H destruct
 | #V #T #T1 #T2 #HT1 #HT12 #i #H destruct /3 width=6/
 | #V #T1 #T2 #HT12 #i #H destruct /3/
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma
index 7bb90c2fc..f3afe6f21 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_lift.ma
@@ -21,14 +21,11 @@ lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 →
                 ∀d,e,U1. ↑[d, e] T1 ≡ U1 → ∀U2. ↑[d, e] T2 ≡ U2 → U1 ⇒ U2.
 #T1 #T2 #H elim H -H T1 T2
 [ #k #d #e #U1 #HU1 #U2 #HU2
-  lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1; 
+  lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1;
   lapply (lift_inv_sort1 … HU2) -HU2 #H destruct -U2 //
 | #i #d #e #U1 #HU1 #U2 #HU2
   lapply (lift_mono … HU1 … HU2) -HU1 #H destruct -U1;
   lapply (lift_inv_lref1 … HU2) * * #Hid #H destruct -U2 //
-| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
-  elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
-  elim (lift_inv_bind1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 /3/
 | #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
   elim (lift_inv_flat1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
   elim (lift_inv_flat1 … HX2) -HX2 #W2 #U2 #HVW2 #HTU2 #HX2 destruct -X2 /3/
@@ -36,7 +33,7 @@ lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 →
   elim (lift_inv_flat1 … HX1) -HX1 #V0 #X #HV10 #HX #HX1 destruct -X1;
   elim (lift_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT10 #HX destruct -X;
   elim (lift_inv_bind1 … HX2) -HX2 #V3 #T3 #HV23 #HT23 #HX2 destruct -X2 /3/
-| #V1 #V2 #T1 #T2 #T0 #HV12 #HT12 #HT2 #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
+| #I #V1 #V2 #T1 #T2 #T0 #HV12 #HT12 #HT2 #IHV12 #IHT12 #d #e #X1 #HX1 #X2 #HX2
   elim (lift_inv_bind1 … HX1) -HX1 #W1 #U1 #HVW1 #HTU1 #HX1 destruct -X1;
   elim (lift_inv_bind1 … HX2) -HX2 #W2 #U0 #HVW2 #HTU0 #HX2 destruct -X2;
   elim (lift_total T2 (d + 1) e) #U2 #HTU2
@@ -64,10 +61,6 @@ lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 →
   lapply (lift_inv_sort2 … HU1) -HU1 #H destruct -U1 /2/
 | #i #d #e #U1 #HU1
   lapply (lift_inv_lref2 … HU1) -HU1 * * #Hid #H destruct -U1 /3/
-| #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX
-  elim (lift_inv_bind2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X;
-  elim (IHV12 … HV01) -IHV12 HV01;
-  elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/
 | #I #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #e #X #HX
   elim (lift_inv_flat2 … HX) -HX #V0 #T0 #HV01 #HT01 #HX destruct -X;
   elim (IHV12 … HV01) -IHV12 HV01;
@@ -77,7 +70,7 @@ lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 →
   elim (lift_inv_bind2 … HY) -HY #W0 #T0 #HW01 #HT01 #HY destruct -Y;
   elim (IHV12 … HV01) -IHV12 HV01;
   elim (IHT12 … HT01) -IHT12 HT01 /3 width=5/
-| #V1 #V2 #T1 #T2 #T0 #_ #_ #HT20 #IHV12 #IHT12 #d #e #X #HX
+| #I #V1 #V2 #T1 #T2 #T0 #_ #_ #HT20 #IHV12 #IHT12 #d #e #X #HX
   elim (lift_inv_bind2 … HX) -HX #W1 #U1 #HWV1 #HUT1 #HX destruct -X;
   elim (IHV12 … HWV1) -IHV12 HWV1 #W2 #HWV2 #HW12
   elim (IHT12 … HUT1) -IHT12 HUT1 #U2 #HUT2 #HU12
@@ -100,3 +93,24 @@ lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 →
   elim (IHT12 … HT01) -IHT12 HT01 /3/
 ]
 qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abst} V1. T1 →
+                         ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2.
+#U1 #U2 * -U1 U2
+[ #k #V #T #H destruct
+| #i #V #T #H destruct
+| #I #V1 #V2 #T1 #T2 #_ #_ #V #T #H destruct
+| #V1 #V2 #W #T1 #T2 #_ #_ #V #T #H destruct
+| #I #V1 #V2 #T1 #T2 #T #HV12 #HT12 #HT2 #V0 #T0 #H destruct -I V1 T1;
+  <(tps_inv_refl1 … HT2 ? ? ?) -HT2 T /2 width=5/
+| #V #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #V0 #T0 #H destruct
+| #V #T #T1 #T2 #_ #_ #V0 #T0 #H destruct
+| #V #T1 #T2 #_ #V0 #T0 #H destruct
+]
+qed.
+
+lemma tpr_inv_abst1: ∀V1,T1,U2. 𝕚{Abst} V1. T1 ⇒ U2 →
+                     ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2.
+/2/ qed.
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma
index aec243d13..d0ae3fa90 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/reduction/tpr_tpr.ma
@@ -26,48 +26,6 @@ lemma tpr_conf_sort_sort: ∀k. ∃∃X. ⋆k ⇒ X & ⋆k ⇒ X.
 lemma tpr_conf_lref_lref: ∀i. ∃∃X. #i ⇒ X & #i ⇒ X.
 /2/ qed.
 
-lemma tpr_conf_bind_bind:
-   ∀I,V0,V1,T0,T1,V2,T2. (
-      ∀X0:term. #X0 < #V0 + #T0 + 1 →
-      ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
-      ∃∃X. X1 ⇒ X & X2 ⇒ X
-   ) →
-   V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
-   ∃∃X. 𝕓{I} V1. T1 ⇒ X & 𝕓{I} V2. T2 ⇒ X.
-#I #V0 #V1 #T0 #T1 #V2 #T2 #IH #HV01 #HV02 #HT01 #HT02
-elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
-elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/
-qed.
-
-lemma tpr_conf_bind_delta:
-   ∀V0,V1,T0,T1,V2,T2,T. (
-      ∀X0:term. #X0 < #V0 + #T0 + 1 →
-      ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
-      ∃∃X. X1 ⇒ X & X2 ⇒ X
-   ) →
-   V0 ⇒ V1 → V0 ⇒ V2 →
-   T0 ⇒ T1 → T0 ⇒ T2 → ⋆. 𝕓{Abbr} V2 ⊢ T2 [O,1] ≫ T →
-   ∃∃X. 𝕓{Abbr} V1. T1 ⇒ X & 𝕓{Abbr} V2. T ⇒ X.
-#V0 #V1 #T0 #T1 #V2 #T2 #T #IH #HV01 #HV02 #HT01 #HT02 #HT2
-elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
-elim (IH … HT01 … HT02) -HT01 HT02 IH // -V0 T0 #T0 #HT10 #HT20
-elim (tpr_tps_bind … HV2 HT20 … HT2) -HT20 HT2 /3 width=5/
-qed.
-
-lemma tpr_conf_bind_zeta:
-   ∀X2,V0,V1,T0,T1,T. (
-      ∀X0:term. #X0 < #V0 + #T0 +1 →
-      ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
-      ∃∃X. X1 ⇒ X & X2 ⇒ X
-   ) →
-   V0 ⇒ V1 → T0 ⇒ T1 → T ⇒ X2 → ↑[O, 1] T ≡ T0 →
-   ∃∃X. 𝕓{Abbr} V1. T1 ⇒ X & X2 ⇒ X.
-#X2 #V0 #V1 #T0 #T1 #T #IH #HV01 #HT01 #HTX2 #HT0
-elim (tpr_inv_lift … HT01 … HT0) -HT01 #U #HUT1 #HTU
-lapply (tw_lift … HT0) -HT0 #HT0
-elim (IH … HTX2 … HTU) -HTX2 HTU IH /3/
-qed.
-
 lemma tpr_conf_flat_flat:
    ∀I,V0,V1,T0,T1,V2,T2. (
       ∀X0:term. #X0 < #V0 + #T0 + 1 →
@@ -110,13 +68,8 @@ elim (IH … HV01 … HV02) -HV01 HV02 // #VV #HVV1 #HVV2
 elim (lift_total VV 0 1) #VVV #HVV
 lapply (tpr_lift … HVV2 … HV2 … HVV) #HVVV
 elim (tpr_inv_abbr1 … H) -H *
-(* case 1: bind *)
-[ -HV2 HVV2 #WW #UU #HWW0 #HUU0 #H destruct -T1;
-  elim (IH … HW02 … HWW0) -HW02 HWW0 // #W #HW2 #HWW
-  elim (IH … HU02 … HUU0) -HU02 HUU0 IH // #U #HU2 #HUU
-  @ex2_1_intro [2: @tpr_theta |1:skip |3: @tpr_bind ] /2 width=7/ (**) (* /4 width=7/ is too slow *)
-(* case 2: delta *)
-| -HV2 HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct -T1;
+(* case 1: delta *)
+[ -HV2 HVV2 #WW2 #UU2 #UU #HWW2 #HUU02 #HUU2 #H destruct -T1;
   elim (IH … HW02 … HWW2) -HW02 HWW2 // #W #HW02 #HWW2
   elim (IH … HU02 … HUU02) -HU02 HUU02 IH // #U #HU2 #HUUU2
   elim (tpr_tps_bind … HWW2 HUUU2 … HUU2) -HUU2 HUUU2 #UUU #HUUU2 #HUUU1
@@ -164,16 +117,16 @@ elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/
 qed.
 
 lemma tpr_conf_delta_delta:
-   ∀V0,V1,T0,T1,TT1,V2,T2,TT2. (
+   ∀I1,V0,V1,T0,T1,TT1,V2,T2,TT2. (
       ∀X0:term. #X0 < #V0 +#T0 + 1→
       ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
       ∃∃X. X1 ⇒ X & X2 ⇒ X
    ) →
    V0 ⇒ V1 → V0 ⇒ V2 → T0 ⇒ T1 → T0 ⇒ T2 →
-   ⋆. 𝕓{Abbr} V1 ⊢ T1 [O, 1] ≫ TT1 →
-   ⋆. 𝕓{Abbr} V2 ⊢ T2 [O, 1] ≫ TT2 →
-   ∃∃X. 𝕓{Abbr} V1. TT1 ⇒ X & 𝕓{Abbr} V2. TT2 ⇒ X.
-#V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2
+   ⋆. 𝕓{I1} V1 ⊢ T1 [O, 1] ≫ TT1 →
+   ⋆. 𝕓{I1} V2 ⊢ T2 [O, 1] ≫ TT2 →
+   ∃∃X. 𝕓{I1} V1. TT1 ⇒ X & 𝕓{I1} V2. TT2 ⇒ X.
+#I1 #V0 #V1 #T0 #T1 #TT1 #V2 #T2 #TT2 #IH #HV01 #HV02 #HT01 #HT02 #HTT1 #HTT2
 elim (IH … HV01 … HV02) -HV01 HV02 // #V #HV1 #HV2
 elim (IH … HT01 … HT02) -HT01 HT02 IH // #T #HT1 #HT2
 elim (tpr_tps_bind … HV1 HT1 … HTT1) -HT1 HTT1 #U1 #TTU1 #HTU1
@@ -262,85 +215,67 @@ lemma tpr_conf_aux:
   lapply (tpr_inv_lref1 … H1) -H1
 (* case 2: lref, lref *)
   #H1 destruct -X2 //
-| #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0;
-  elim (tpr_inv_bind1 … H1) -H1 *
-(* case 3: bind, bind *)
-  [ #V2 #T2 #HV02 #HT02 #H destruct -X2
-    /3 width=7 by tpr_conf_bind_bind/ (**) (* /3 width=7/ is too slow *)
-(* case 4: bind, delta *)
-  | #V2 #T2 #T #HV02 #HT02 #HT2 #H1 #H2 destruct -X2 I
-    /3 width=9 by tpr_conf_bind_delta/ (**) (* /3 width=9/ is too slow *)
-(* case 5: bind, zeta *)
-  | #T #HT0 #HTX2 #H destruct -I
-    /3 width=8 by tpr_conf_bind_zeta/ (**) (* /3 width=8/ is too slow *)
-  ]
 | #I #V0 #V1 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0;
   elim (tpr_inv_flat1 … H1) -H1 *
-(* case 6: flat, flat *)
+(* case 3: flat, flat *)
   [ #V2 #T2 #HV02 #HT02 #H destruct -X2
     /3 width=7 by tpr_conf_flat_flat/ (**) (* /3 width=7/ is too slow *)
-(* case 7: flat, beta *)
+(* case 4: flat, beta *)
   | #V2 #W #U0 #T2 #HV02 #HT02 #H1 #H2 #H3 destruct -T0 X2 I
     /3 width=8 by tpr_conf_flat_beta/ (**) (* /3 width=8/ is too slow *)
-(* case 8: flat, theta *)
+(* case 5: flat, theta *)
   | #V2 #V #W0 #W2 #U0 #U2 #HV02 #HW02 #HT02 #HV2 #H1 #H2 #H3 destruct -T0 X2 I
     /3 width=11 by tpr_conf_flat_theta/ (**) (* /3 width=11/ is too slow *)
-(* case 9: flat, tau *)
+(* case 6: flat, tau *)
   | #HT02 #H destruct -I
     /3 width=6 by tpr_conf_flat_cast/ (**) (* /3 width=6/ is too slow *)
   ]
 | #V0 #V1 #W0 #T0 #T1 #HV01 #HT01 #H1 #H2 destruct -Y0;
   elim (tpr_inv_appl1 … H1) -H1 *
-(* case 10: beta, flat (repeated) *)
+(* case 7: beta, flat (repeated) *)
   [ #V2 #T2 #HV02 #HT02 #H destruct -X2
     @ex2_1_comm /3 width=8 by tpr_conf_flat_beta/
-(* case 11: beta, beta *)
+(* case 8: beta, beta *)
   | #V2 #WW0 #TT0 #T2 #HV02 #HT02 #H1 #H2 destruct -W0 T0 X2
     /3 width=8 by tpr_conf_beta_beta/ (**) (* /3 width=8/ is too slow *)
-(* case 12, beta, theta (excluded) *)
+(* case 9, beta, theta (excluded) *)
   | #V2 #VV2 #WW0 #W2 #TT0 #T2 #_ #_ #_ #_ #H destruct
   ]
-| #V0 #V1 #T0 #T1 #TT1 #HV01 #HT01 #HTT1 #H1 #H2 destruct -Y0;
-  elim (tpr_inv_abbr1 … H1) -H1 *
-(* case 13: delta, bind (repeated) *)
-  [ #V2 #T2 #HV02 #T02 #H destruct -X2
-    @ex2_1_comm /3 width=9 by tpr_conf_bind_delta/
-(* case 14: delta, delta *)
-  | #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2
+| #I1 #V0 #V1 #T0 #T1 #TT1 #HV01 #HT01 #HTT1 #H1 #H2 destruct -Y0;
+  elim (tpr_inv_bind1 … H1) -H1 *
+(* case 10: delta, delta *)
+  [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2
     /3 width=11 by tpr_conf_delta_delta/ (**) (* /3 width=11/ is too slow *)
-(* case 15: delta, zata *)
-  | #T2 #HT20 #HTX2
+(* case 11: delta, zata *)
+  | #T2 #HT20 #HTX2 #H destruct -I1;
     /3 width=10 by tpr_conf_delta_zeta/ (**) (* /3 width=10/ is too slow *)
   ]
 | #VV1 #V0 #V1 #W0 #W1 #T0 #T1 #HV01 #HVV1 #HW01 #HT01 #H1 #H2 destruct -Y0;
   elim (tpr_inv_appl1 … H1) -H1 *
-(* case 16: theta, flat (repeated) *)
+(* case 12: theta, flat (repeated) *)
   [ #V2 #T2 #HV02 #HT02 #H destruct -X2
     @ex2_1_comm /3 width=11 by tpr_conf_flat_theta/
-(* case 17: theta, beta (repeated) *)
+(* case 13: theta, beta (repeated) *)
   | #V2 #WW0 #TT0 #T2 #_ #_ #H destruct
-(* case 18: theta, theta *)
+(* case 14: theta, theta *)
   | #V2 #VV2 #WW0 #W2 #TT0 #T2 #V02 #HW02 #HT02 #HVV2 #H1 #H2 destruct -W0 T0 X2
-    /3 width=14 by tpr_conf_theta_theta/  (**) (* /3 width=14/ is too slow *)
+    /3 width=14 by tpr_conf_theta_theta/ (**) (* /3 width=14/ is too slow *)
   ]
 | #V0 #TT0 #T0 #T1 #HTT0 #HT01 #H1 #H2 destruct -Y0;
   elim (tpr_inv_abbr1 … H1) -H1 *
-(* case 19: zeta, bind (repeated) *)
-  [ #V2 #T2 #HV02 #T02 #H destruct -X2
-    @ex2_1_comm /3 width=8 by tpr_conf_bind_zeta/
-(* case 20: zeta, delta (repeated) *)
-  | #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2
+(* case 15: zeta, delta (repeated) *)
+  [ #V2 #T2 #TT2 #HV02 #HT02 #HTT2 #H destruct -X2
     @ex2_1_comm /3 width=10 by tpr_conf_delta_zeta/
-(* case 21: zeta, zeta *)
+(* case 16: zeta, zeta *)
   | #T2 #HTT20 #HTX2
     /3 width=9 by tpr_conf_zeta_zeta/ (**) (* /3 width=9/ is too slow *)
   ] 
 | #V0 #T0 #T1 #HT01 #H1 #H2 destruct -Y0;
   elim (tpr_inv_cast1 … H1) -H1
-(* case 22: tau, flat (repeated) *)
+(* case 17: tau, flat (repeated) *)
   [ * #V2 #T2 #HV02 #HT02 #H destruct -X2
     @ex2_1_comm /3 width=6 by tpr_conf_flat_cast/
-(* case 23: tau, tau *)
+(* case 18: tau, tau *)
   | #HT02
     /2 by tpr_conf_tau_tau/
   ]
diff --git a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma
index d15b59535..24571a88f 100644
--- a/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma
+++ b/matita/matita/contribs/lambda-delta/Basic-2/substitution/tps_lift.ma
@@ -181,3 +181,24 @@ lapply (tps_weak … HU1 d e ? ?) -HU1 // <plus_minus_m_m_comm // -Hddt Hdtde #H
 lapply (tps_inv_lift1_eq … HU1 … HTU1) -HU1 #HU1 destruct -U1;
 elim (tps_inv_lift1_ge … HU2 … HLK … HTU1 ?) -HU2 HLK HTU1 // <minus_plus_m_m /2/
 qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma tps_inv_refl1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 1 →
+                         ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
+#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
+[ //
+| //
+| #L #K0 #V0 #W #i #d #e #Hdi #Hide #HLK0 #_ #H destruct -e;
+  >(le_to_le_to_eq … Hdi ?) /2/ -d #K #V #HLK
+  lapply (drop_mono … HLK0 … HLK) #H destruct
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK
+  >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 K V) -IHT12 /2/
+| #L #I #V1 #V2 #T1 #T2 #d #e #_ #_ #IHV12 #IHT12 #H1 #K #V #HLK
+  >(IHV12 H1 … HLK) -IHV12 >(IHT12 H1 … HLK) -IHT12 //
+]
+qed.
+
+lemma tps_inv_refl1: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫ T2 →
+                     ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
+/2 width=8/ qed.