X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Ftpr.ma;h=957b5f3a89926458ddf3feaa3371b7bc68766e0d;hb=1f1ea7bb9e6c34626bcabd4c0142fcde98bcbbe5;hp=a74757b2a17c7b36ea4f6b65d61681e13be89f32;hpb=f6464ba2cffc9936b4d8285604786cd91531e0d0;p=helm.git

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma
index a74757b2a..957b5f3a8 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma
@@ -206,33 +206,23 @@ lemma tpr_inv_lref2: ∀T1,i. T1 ➡ #i →
 (* Basic forward lemmas *****************************************************)
 
 lemma tpr_fwd_shift1: ∀L1,T1,T. L1 @@ T1 ➡ T →
-                      ∃∃L2,T2. L1 𝟙 L2 & T = L2 @@ T2.
-#L1 @(lenv_ind_dx … L1) -L1
-[ #T1 #T #_ @ex2_2_intro [3: // |4: // |1,2: skip ] (**) (* /2 width=4/ does not work *)
-| #I #L1 #V1 #IH #T1 #T >shift_append_assoc #H
+                      ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
+#L1 @(lenv_ind_dx … L1) -L1 normalize
+[ #T1 #T #HT1
+  @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
+| #I #L1 #V1 #IH #T1 #X
+  >shift_append_assoc normalize #H
   elim (tpr_inv_bind1 … H) -H *
-  [ #V0 #T0 #X0 #_ #HT10 #HTX0 #H destruct
-    elim (IH … HT10) -IH -T1 #L2 #V2 #HL12 #H destruct
-    elim (tps_fwd_shift1 … HTX0) -V2 #L3 #X3 #HL23 #H destruct
-    lapply (ltop_trans … HL12 HL23) -L2 #HL13
-    @(ex2_2_intro … (⋆.ⓑ{I}V0@@L3)) /2 width=4/ /3 width=1/
-  | #T0 #_ #_ #H destruct
+  [ #V0 #T0 #X0 #_ #HT10 #H0 #H destruct
+    elim (IH … HT10) -IH -T1 #L #T #HL1 #H destruct
+    elim (tps_fwd_shift1 … H0) -T #L2 #T2 #HL2 #H destruct
+    >append_length >HL1 >HL2 -L1 -L
+    @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *)
+  | #T #_ #_ #H destruct
   ]
 ]
 qed-.
 
-lemma tpr_fwd_shift_bind_minus: ∀L1,L2. |L1| = |L2| → ∀I1,I2,V1,V2,T1,T2.
-                                L1 @@ -ⓑ{I1}V1.T1 ➡ L2 @@ -ⓑ{I2}V2.T2 →
-                                L1 𝟙 L2 ∧ I1 = I2.
-#L1 #L2 #HL12 #I1 #I2 #V1 #V2 #T1 #T2 #H
-elim (tpr_fwd_shift1 (L1.ⓑ{I1}V1) … H) -H #Y #X #HY #HX
-elim (ltop_inv_pair1 … HY) -HY #L #V #HL1 #H destruct
-elim (shift_inj (L2.ⓑ{I2}V2) … HX ?) -HX
-[ #H1 #_ destruct /2 width=1/
-| lapply (ltop_fwd_length … HL1) -HL1 normalize // 
-]
-qed-.
-
 (* Basic_1: removed theorems 3:
             pr0_subst0_back pr0_subst0_fwd pr0_subst0
    Basic_1: removed local theorems: 1: pr0_delta_tau