X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Ftpr.ma;fp=matita%2Fmatita%2Fcontribs%2Flambda_delta%2Fbasic_2%2Freducibility%2Ftpr.ma;h=a74757b2a17c7b36ea4f6b65d61681e13be89f32;hb=f6464ba2cffc9936b4d8285604786cd91531e0d0;hp=d204eba79add94bd571ffb62aa04a91a47941205;hpb=abed266f42c25bf77c5c4bfbff0450abe9680e7a;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 d204eba79..a74757b2a 100644
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma
@@ -203,6 +203,36 @@ lemma tpr_inv_lref2: ∀T1,i. T1 ➡ #i →
                       | ∃∃V,T. T ➡ #i & T1 = ⓝV. T.
 /2 width=3/ qed-.
 
+(* 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
+  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
+  ]
+]
+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